Theorem reclem4pr 9474

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 9472	. . . . . 6 |- ( A e. P. -> B e. P. )
3		df-mp 9408	. . . . . . 7 |- .P. = ( y e. P. , w e. P. |-> { u | E. f e. y E. g e. w u = ( f .Q g ) } )
4		mulclnq 9371	. . . . . . 7 |- ( ( f e. Q. /\ g e. Q. ) -> ( f .Q g ) e. Q. )
5	3, 4	genpelv 9424	. . . . . 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 672	. . . . 5 |- ( A e. P. -> ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
7	1	abeq2i 2556	. . . . . . . . 9 |- ( x e. B <-> E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) )
8		ltrelnq 9350	. . . . . . . . . . . . . . 15 |- <Q C_ ( Q. X. Q. )
9	8	brel 4903	. . . . . . . . . . . . . 14 |- ( x <Q y -> ( x e. Q. /\ y e. Q. ) )
10	9	simprd 464	. . . . . . . . . . . . 13 |- ( x <Q y -> y e. Q. )
11		elprnq 9415	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. P. /\ z e. A ) -> z e. Q. )
12		ltmnq 9396	. . . . . . . . . . . . . . . . . . 19 |- ( z e. Q. -> ( x <Q y <-> ( z .Q x ) <Q ( z .Q y ) ) )
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. P. /\ z e. A ) -> ( x <Q y <-> ( z .Q x ) <Q ( z .Q y ) ) )
14	13	biimpd 210	. . . . . . . . . . . . . . . . 17 |- ( ( A e. P. /\ z e. A ) -> ( x <Q y -> ( z .Q x ) <Q ( z .Q y ) ) )
15	14	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( x <Q y -> ( z .Q x ) <Q ( z .Q y ) ) )
16		recclnq 9390	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> ( *Q ` y ) e. Q. )
17		prub 9418	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. P. /\ z e. A ) /\ ( *Q ` y ) e. Q. ) -> ( -. ( *Q ` y ) e. A -> z <Q ( *Q ` y ) ) )
18	16, 17	sylan2 476	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( -. ( *Q ` y ) e. A -> z <Q ( *Q ` y ) ) )
19		ltmnq 9396	. . . . . . . . . . . . . . . . . . 19 |- ( y e. Q. -> ( z <Q ( *Q ` y ) <-> ( y .Q z ) <Q ( y .Q ( *Q ` y ) ) ) )
20		mulcomnq 9377	. . . . . . . . . . . . . . . . . . . . 21 |- ( y .Q z ) = ( z .Q y )
21	20	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. Q. -> ( y .Q z ) = ( z .Q y ) )
22		recidnq 9389	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. Q. -> ( y .Q ( *Q ` y ) ) = 1Q )
23	21, 22	breq12d 4439	. . . . . . . . . . . . . . . . . . 19 |- ( y e. Q. -> ( ( y .Q z ) <Q ( y .Q ( *Q ` y ) ) <-> ( z .Q y ) <Q 1Q ) )
24	19, 23	bitrd 256	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> ( z <Q ( *Q ` y ) <-> ( z .Q y ) <Q 1Q ) )
25	24	adantl 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( z <Q ( *Q ` y ) <-> ( z .Q y ) <Q 1Q ) )
26	18, 25	sylibd 217	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( -. ( *Q ` y ) e. A -> ( z .Q y ) <Q 1Q ) )
27	15, 26	anim12d 565	. . . . . . . . . . . . . . 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 9393	. . . . . . . . . . . . . . . 16 |- <Q Or Q.
29	28, 8	sotri 5247	. . . . . . . . . . . . . . 15 |- ( ( ( z .Q x ) <Q ( z .Q y ) /\ ( z .Q y ) <Q 1Q ) -> ( z .Q x ) <Q 1Q )
30	27, 29	syl6 34	. . . . . . . . . . . . . 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 610	. . . . . . . . . . . . 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 33	. . . . . . . . . . . 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 50	. . . . . . . . . . 11 |- ( ( A e. P. /\ z e. A ) -> ( x <Q y -> ( -. ( *Q ` y ) e. A -> ( z .Q x ) <Q 1Q ) ) )
34	33	impd 432	. . . . . . . . . 10 |- ( ( A e. P. /\ z e. A ) -> ( ( x <Q y /\ -. ( *Q ` y ) e. A ) -> ( z .Q x ) <Q 1Q ) )
35	34	exlimdv 1771	. . . . . . . . 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 220	. . . . . . . 8 |- ( ( A e. P. /\ z e. A ) -> ( x e. B -> ( z .Q x ) <Q 1Q ) )
37		breq1 4429	. . . . . . . . 9 |- ( w = ( z .Q x ) -> ( w <Q 1Q <-> ( z .Q x ) <Q 1Q ) )
38	37	biimprcd 228	. . . . . . . 8 |- ( ( z .Q x ) <Q 1Q -> ( w = ( z .Q x ) -> w <Q 1Q ) )
39	36, 38	syl6 34	. . . . . . 7 |- ( ( A e. P. /\ z e. A ) -> ( x e. B -> ( w = ( z .Q x ) -> w <Q 1Q ) ) )
40	39	expimpd 606	. . . . . 6 |- ( A e. P. -> ( ( z e. A /\ x e. B ) -> ( w = ( z .Q x ) -> w <Q 1Q ) ) )
41	40	rexlimdvv 2930	. . . . 5 |- ( A e. P. -> ( E. z e. A E. x e. B w = ( z .Q x ) -> w <Q 1Q ) )
42	6, 41	sylbid 218	. . . 4 |- ( A e. P. -> ( w e. ( A .P. B ) -> w <Q 1Q ) )
43		df-1p 9406	. . . . 5 |- 1P = { w | w <Q 1Q }
44	43	abeq2i 2556	. . . 4 |- ( w e. 1P <-> w <Q 1Q )
45	42, 44	syl6ibr 230	. . 3 |- ( A e. P. -> ( w e. ( A .P. B ) -> w e. 1P ) )
46	45	ssrdv 3476	. 2 |- ( A e. P. -> ( A .P. B ) C_ 1P )
47	1	reclem3pr 9473	. 2 |- ( A e. P. -> 1P C_ ( A .P. B ) )
48	46, 47	eqssd 3487	1 |- ( A e. P. -> ( A .P. B ) = 1P )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1870   {cab 2414   E.wrex 2783   class class class wbr 4426   ` cfv 5601  (class class class)co 6305   Q.cnq 9276   1Qc1q 9277   .Q cmq 9280   *Qcrq 9281   <Q cltq 9282   P.cnp 9283   1Pc1p 9284   .P. cmp 9286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-inf2 8146

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-omul 7195  df-er 7371  df-ni 9296  df-pli 9297  df-mi 9298  df-lti 9299  df-plpq 9332  df-mpq 9333  df-ltpq 9334  df-enq 9335  df-nq 9336  df-erq 9337  df-plq 9338  df-mq 9339  df-1nq 9340  df-rq 9341  df-ltnq 9342  df-np 9405  df-1p 9406  df-mp 9408

This theorem is referenced by:  recexpr  9475