Theorem reclem4pr 9361

Description: Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (New usage is discouraged.)

Hypothesis

Ref	Expression
reclempr.1	|- B = { x | E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) }

Assertion

Ref	Expression
reclem4pr	|- ( A e. P. -> ( A .P. B ) = 1P )

Distinct variable groups:   x, y, A   x, B

Allowed substitution hint:   B( y)

Proof of Theorem reclem4pr

Dummy variables z w u f g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reclempr.1	. . . . . . 7 |- B = { x | E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) }
2	1	reclem2pr 9359	. . . . . 6 |- ( A e. P. -> B e. P. )
3		df-mp 9295	. . . . . . 7 |- .P. = ( y e. P. , w e. P. |-> { u | E. f e. y E. g e. w u = ( f .Q g ) } )
4		mulclnq 9258	. . . . . . 7 |- ( ( f e. Q. /\ g e. Q. ) -> ( f .Q g ) e. Q. )
5	3, 4	genpelv 9311	. . . . . 6 |- ( ( A e. P. /\ B e. P. ) -> ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
6	2, 5	mpdan 666	. . . . 5 |- ( A e. P. -> ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
7	1	abeq2i 2523	. . . . . . . . 9 |- ( x e. B <-> E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) )
8		ltrelnq 9237	. . . . . . . . . . . . . . 15 |- <Q C_ ( Q. X. Q. )
9	8	brel 4979	. . . . . . . . . . . . . 14 |- ( x <Q y -> ( x e. Q. /\ y e. Q. ) )
10	9	simprd 461	. . . . . . . . . . . . 13 |- ( x <Q y -> y e. Q. )
11		elprnq 9302	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. P. /\ z e. A ) -> z e. Q. )
12		ltmnq 9283	. . . . . . . . . . . . . . . . . . 19 |- ( z e. Q. -> ( x <Q y <-> ( z .Q x ) <Q ( z .Q y ) ) )
13	11, 12	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. P. /\ z e. A ) -> ( x <Q y <-> ( z .Q x ) <Q ( z .Q y ) ) )
14	13	biimpd 207	. . . . . . . . . . . . . . . . 17 |- ( ( A e. P. /\ z e. A ) -> ( x <Q y -> ( z .Q x ) <Q ( z .Q y ) ) )
15	14	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( x <Q y -> ( z .Q x ) <Q ( z .Q y ) ) )
16		recclnq 9277	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> ( *Q ` y ) e. Q. )
17		prub 9305	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. P. /\ z e. A ) /\ ( *Q ` y ) e. Q. ) -> ( -. ( *Q ` y ) e. A -> z <Q ( *Q ` y ) ) )
18	16, 17	sylan2 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( -. ( *Q ` y ) e. A -> z <Q ( *Q ` y ) ) )
19		ltmnq 9283	. . . . . . . . . . . . . . . . . . 19 |- ( y e. Q. -> ( z <Q ( *Q ` y ) <-> ( y .Q z ) <Q ( y .Q ( *Q ` y ) ) ) )
20		mulcomnq 9264	. . . . . . . . . . . . . . . . . . . . 21 |- ( y .Q z ) = ( z .Q y )
21	20	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. Q. -> ( y .Q z ) = ( z .Q y ) )
22		recidnq 9276	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. Q. -> ( y .Q ( *Q ` y ) ) = 1Q )
23	21, 22	breq12d 4397	. . . . . . . . . . . . . . . . . . 19 |- ( y e. Q. -> ( ( y .Q z ) <Q ( y .Q ( *Q ` y ) ) <-> ( z .Q y ) <Q 1Q ) )
24	19, 23	bitrd 253	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> ( z <Q ( *Q ` y ) <-> ( z .Q y ) <Q 1Q ) )
25	24	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( z <Q ( *Q ` y ) <-> ( z .Q y ) <Q 1Q ) )
26	18, 25	sylibd 214	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( -. ( *Q ` y ) e. A -> ( z .Q y ) <Q 1Q ) )
27	15, 26	anim12d 561	. . . . . . . . . . . . . . 15 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( ( x <Q y /\ -. ( *Q ` y ) e. A ) -> ( ( z .Q x ) <Q ( z .Q y ) /\ ( z .Q y ) <Q 1Q ) ) )
28		ltsonq 9280	. . . . . . . . . . . . . . . 16 |- <Q Or Q.
29	28, 8	sotri 5324	. . . . . . . . . . . . . . 15 |- ( ( ( z .Q x ) <Q ( z .Q y ) /\ ( z .Q y ) <Q 1Q ) -> ( z .Q x ) <Q 1Q )
30	27, 29	syl6 33	. . . . . . . . . . . . . 14 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( ( x <Q y /\ -. ( *Q ` y ) e. A ) -> ( z .Q x ) <Q 1Q ) )
31	30	exp4b 605	. . . . . . . . . . . . 13 |- ( ( A e. P. /\ z e. A ) -> ( y e. Q. -> ( x <Q y -> ( -. ( *Q ` y ) e. A -> ( z .Q x ) <Q 1Q ) ) ) )
32	10, 31	syl5 32	. . . . . . . . . . . 12 |- ( ( A e. P. /\ z e. A ) -> ( x <Q y -> ( x <Q y -> ( -. ( *Q ` y ) e. A -> ( z .Q x ) <Q 1Q ) ) ) )
33	32	pm2.43d 48	. . . . . . . . . . 11 |- ( ( A e. P. /\ z e. A ) -> ( x <Q y -> ( -. ( *Q ` y ) e. A -> ( z .Q x ) <Q 1Q ) ) )
34	33	impd 429	. . . . . . . . . 10 |- ( ( A e. P. /\ z e. A ) -> ( ( x <Q y /\ -. ( *Q ` y ) e. A ) -> ( z .Q x ) <Q 1Q ) )
35	34	exlimdv 1739	. . . . . . . . 9 |- ( ( A e. P. /\ z e. A ) -> ( E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) -> ( z .Q x ) <Q 1Q ) )
36	7, 35	syl5bi 217	. . . . . . . 8 |- ( ( A e. P. /\ z e. A ) -> ( x e. B -> ( z .Q x ) <Q 1Q ) )
37		breq1 4387	. . . . . . . . 9 |- ( w = ( z .Q x ) -> ( w <Q 1Q <-> ( z .Q x ) <Q 1Q ) )
38	37	biimprcd 225	. . . . . . . 8 |- ( ( z .Q x ) <Q 1Q -> ( w = ( z .Q x ) -> w <Q 1Q ) )
39	36, 38	syl6 33	. . . . . . 7 |- ( ( A e. P. /\ z e. A ) -> ( x e. B -> ( w = ( z .Q x ) -> w <Q 1Q ) ) )
40	39	expimpd 601	. . . . . 6 |- ( A e. P. -> ( ( z e. A /\ x e. B ) -> ( w = ( z .Q x ) -> w <Q 1Q ) ) )
41	40	rexlimdvv 2894	. . . . 5 |- ( A e. P. -> ( E. z e. A E. x e. B w = ( z .Q x ) -> w <Q 1Q ) )
42	6, 41	sylbid 215	. . . 4 |- ( A e. P. -> ( w e. ( A .P. B ) -> w <Q 1Q ) )
43		df-1p 9293	. . . . 5 |- 1P = { w | w <Q 1Q }
44	43	abeq2i 2523	. . . 4 |- ( w e. 1P <-> w <Q 1Q )
45	42, 44	syl6ibr 227	. . 3 |- ( A e. P. -> ( w e. ( A .P. B ) -> w e. 1P ) )
46	45	ssrdv 3440	. 2 |- ( A e. P. -> ( A .P. B ) C_ 1P )
47	1	reclem3pr 9360	. 2 |- ( A e. P. -> 1P C_ ( A .P. B ) )
48	46, 47	eqssd 3451	1 |- ( A e. P. -> ( A .P. B ) = 1P )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   E.wex 1627   e. wcel 1836   {cab 2381   E.wrex 2747   class class class wbr 4384   ` cfv 5513  (class class class)co 6218   Q.cnq 9163   1Qc1q 9164   .Q cmq 9167   *Qcrq 9168   <Q cltq 9169   P.cnp 9170   1Pc1p 9171   .P. cmp 9173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-inf2 7994

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-1st 6721  df-2nd 6722  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-omul 7075  df-er 7251  df-ni 9183  df-pli 9184  df-mi 9185  df-lti 9186  df-plpq 9219  df-mpq 9220  df-ltpq 9221  df-enq 9222  df-nq 9223  df-erq 9224  df-plq 9225  df-mq 9226  df-1nq 9227  df-rq 9228  df-ltnq 9229  df-np 9292  df-1p 9293  df-mp 9295

This theorem is referenced by:  recexpr  9362