Metamath Proof Explorer


Theorem reclem3pr

Description: Lemma for Proposition 9-3.7(v) of Gleason p. 124. (Contributed by NM, 30-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypothesis reclempr.1 B = x | y x < 𝑸 y ¬ * 𝑸 y A
Assertion reclem3pr A 𝑷 1 𝑷 A 𝑷 B

Proof

Step Hyp Ref Expression
1 reclempr.1 B = x | y x < 𝑸 y ¬ * 𝑸 y A
2 df-1p 1 𝑷 = w | w < 𝑸 1 𝑸
3 2 abeq2i w 1 𝑷 w < 𝑸 1 𝑸
4 ltrnq w < 𝑸 1 𝑸 * 𝑸 1 𝑸 < 𝑸 * 𝑸 w
5 mulcomnq * 𝑸 1 𝑸 𝑸 1 𝑸 = 1 𝑸 𝑸 * 𝑸 1 𝑸
6 1nq 1 𝑸 𝑸
7 recclnq 1 𝑸 𝑸 * 𝑸 1 𝑸 𝑸
8 mulidnq * 𝑸 1 𝑸 𝑸 * 𝑸 1 𝑸 𝑸 1 𝑸 = * 𝑸 1 𝑸
9 6 7 8 mp2b * 𝑸 1 𝑸 𝑸 1 𝑸 = * 𝑸 1 𝑸
10 recidnq 1 𝑸 𝑸 1 𝑸 𝑸 * 𝑸 1 𝑸 = 1 𝑸
11 6 10 ax-mp 1 𝑸 𝑸 * 𝑸 1 𝑸 = 1 𝑸
12 5 9 11 3eqtr3i * 𝑸 1 𝑸 = 1 𝑸
13 12 breq1i * 𝑸 1 𝑸 < 𝑸 * 𝑸 w 1 𝑸 < 𝑸 * 𝑸 w
14 4 13 bitri w < 𝑸 1 𝑸 1 𝑸 < 𝑸 * 𝑸 w
15 prlem936 A 𝑷 1 𝑸 < 𝑸 * 𝑸 w v A ¬ v 𝑸 * 𝑸 w A
16 14 15 sylan2b A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A
17 prnmax A 𝑷 v A z A v < 𝑸 z
18 17 ad2ant2r A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A z A v < 𝑸 z
19 elprnq A 𝑷 v A v 𝑸
20 19 ad2ant2r A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v 𝑸
21 20 3adant3 A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z v 𝑸
22 simp1r A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z w < 𝑸 1 𝑸
23 ltrelnq < 𝑸 𝑸 × 𝑸
24 23 brel w < 𝑸 1 𝑸 w 𝑸 1 𝑸 𝑸
25 24 simpld w < 𝑸 1 𝑸 w 𝑸
26 22 25 syl A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z w 𝑸
27 simp3 A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z v < 𝑸 z
28 simp2r A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z ¬ v 𝑸 * 𝑸 w A
29 ltrnq v < 𝑸 z * 𝑸 z < 𝑸 * 𝑸 v
30 fvex * 𝑸 z V
31 fvex * 𝑸 v V
32 ltmnq u 𝑸 x < 𝑸 y u 𝑸 x < 𝑸 u 𝑸 y
33 vex w V
34 mulcomnq x 𝑸 y = y 𝑸 x
35 30 31 32 33 34 caovord2 w 𝑸 * 𝑸 z < 𝑸 * 𝑸 v * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w
36 29 35 syl5bb w 𝑸 v < 𝑸 z * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w
37 36 adantl v 𝑸 w 𝑸 v < 𝑸 z * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w
38 37 biimpd v 𝑸 w 𝑸 v < 𝑸 z * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w
39 mulcomnq v 𝑸 * 𝑸 v = * 𝑸 v 𝑸 v
40 recidnq v 𝑸 v 𝑸 * 𝑸 v = 1 𝑸
41 39 40 eqtr3id v 𝑸 * 𝑸 v 𝑸 v = 1 𝑸
42 recidnq w 𝑸 w 𝑸 * 𝑸 w = 1 𝑸
43 41 42 oveqan12d v 𝑸 w 𝑸 * 𝑸 v 𝑸 v 𝑸 w 𝑸 * 𝑸 w = 1 𝑸 𝑸 1 𝑸
44 vex v V
45 mulassnq x 𝑸 y 𝑸 u = x 𝑸 y 𝑸 u
46 fvex * 𝑸 w V
47 31 44 33 34 45 46 caov4 * 𝑸 v 𝑸 v 𝑸 w 𝑸 * 𝑸 w = * 𝑸 v 𝑸 w 𝑸 v 𝑸 * 𝑸 w
48 mulidnq 1 𝑸 𝑸 1 𝑸 𝑸 1 𝑸 = 1 𝑸
49 6 48 ax-mp 1 𝑸 𝑸 1 𝑸 = 1 𝑸
50 43 47 49 3eqtr3g v 𝑸 w 𝑸 * 𝑸 v 𝑸 w 𝑸 v 𝑸 * 𝑸 w = 1 𝑸
51 recclnq v 𝑸 * 𝑸 v 𝑸
52 mulclnq * 𝑸 v 𝑸 w 𝑸 * 𝑸 v 𝑸 w 𝑸
53 51 52 sylan v 𝑸 w 𝑸 * 𝑸 v 𝑸 w 𝑸
54 recmulnq * 𝑸 v 𝑸 w 𝑸 * 𝑸 * 𝑸 v 𝑸 w = v 𝑸 * 𝑸 w * 𝑸 v 𝑸 w 𝑸 v 𝑸 * 𝑸 w = 1 𝑸
55 53 54 syl v 𝑸 w 𝑸 * 𝑸 * 𝑸 v 𝑸 w = v 𝑸 * 𝑸 w * 𝑸 v 𝑸 w 𝑸 v 𝑸 * 𝑸 w = 1 𝑸
56 50 55 mpbird v 𝑸 w 𝑸 * 𝑸 * 𝑸 v 𝑸 w = v 𝑸 * 𝑸 w
57 56 eleq1d v 𝑸 w 𝑸 * 𝑸 * 𝑸 v 𝑸 w A v 𝑸 * 𝑸 w A
58 57 notbid v 𝑸 w 𝑸 ¬ * 𝑸 * 𝑸 v 𝑸 w A ¬ v 𝑸 * 𝑸 w A
59 58 biimprd v 𝑸 w 𝑸 ¬ v 𝑸 * 𝑸 w A ¬ * 𝑸 * 𝑸 v 𝑸 w A
60 38 59 anim12d v 𝑸 w 𝑸 v < 𝑸 z ¬ v 𝑸 * 𝑸 w A * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w ¬ * 𝑸 * 𝑸 v 𝑸 w A
61 ovex * 𝑸 v 𝑸 w V
62 breq2 y = * 𝑸 v 𝑸 w * 𝑸 z 𝑸 w < 𝑸 y * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w
63 fveq2 y = * 𝑸 v 𝑸 w * 𝑸 y = * 𝑸 * 𝑸 v 𝑸 w
64 63 eleq1d y = * 𝑸 v 𝑸 w * 𝑸 y A * 𝑸 * 𝑸 v 𝑸 w A
65 64 notbid y = * 𝑸 v 𝑸 w ¬ * 𝑸 y A ¬ * 𝑸 * 𝑸 v 𝑸 w A
66 62 65 anbi12d y = * 𝑸 v 𝑸 w * 𝑸 z 𝑸 w < 𝑸 y ¬ * 𝑸 y A * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w ¬ * 𝑸 * 𝑸 v 𝑸 w A
67 61 66 spcev * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w ¬ * 𝑸 * 𝑸 v 𝑸 w A y * 𝑸 z 𝑸 w < 𝑸 y ¬ * 𝑸 y A
68 ovex * 𝑸 z 𝑸 w V
69 breq1 x = * 𝑸 z 𝑸 w x < 𝑸 y * 𝑸 z 𝑸 w < 𝑸 y
70 69 anbi1d x = * 𝑸 z 𝑸 w x < 𝑸 y ¬ * 𝑸 y A * 𝑸 z 𝑸 w < 𝑸 y ¬ * 𝑸 y A
71 70 exbidv x = * 𝑸 z 𝑸 w y x < 𝑸 y ¬ * 𝑸 y A y * 𝑸 z 𝑸 w < 𝑸 y ¬ * 𝑸 y A
72 68 71 1 elab2 * 𝑸 z 𝑸 w B y * 𝑸 z 𝑸 w < 𝑸 y ¬ * 𝑸 y A
73 67 72 sylibr * 𝑸 z 𝑸 w < 𝑸 * 𝑸 v 𝑸 w ¬ * 𝑸 * 𝑸 v 𝑸 w A * 𝑸 z 𝑸 w B
74 60 73 syl6 v 𝑸 w 𝑸 v < 𝑸 z ¬ v 𝑸 * 𝑸 w A * 𝑸 z 𝑸 w B
75 74 imp v 𝑸 w 𝑸 v < 𝑸 z ¬ v 𝑸 * 𝑸 w A * 𝑸 z 𝑸 w B
76 21 26 27 28 75 syl22anc A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z * 𝑸 z 𝑸 w B
77 23 brel v < 𝑸 z v 𝑸 z 𝑸
78 77 simprd v < 𝑸 z z 𝑸
79 78 3ad2ant3 A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z z 𝑸
80 mulidnq w 𝑸 w 𝑸 1 𝑸 = w
81 mulcomnq w 𝑸 1 𝑸 = 1 𝑸 𝑸 w
82 80 81 eqtr3di w 𝑸 w = 1 𝑸 𝑸 w
83 recidnq z 𝑸 z 𝑸 * 𝑸 z = 1 𝑸
84 83 oveq1d z 𝑸 z 𝑸 * 𝑸 z 𝑸 w = 1 𝑸 𝑸 w
85 mulassnq z 𝑸 * 𝑸 z 𝑸 w = z 𝑸 * 𝑸 z 𝑸 w
86 84 85 eqtr3di z 𝑸 1 𝑸 𝑸 w = z 𝑸 * 𝑸 z 𝑸 w
87 82 86 sylan9eqr z 𝑸 w 𝑸 w = z 𝑸 * 𝑸 z 𝑸 w
88 79 26 87 syl2anc A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z w = z 𝑸 * 𝑸 z 𝑸 w
89 oveq2 x = * 𝑸 z 𝑸 w z 𝑸 x = z 𝑸 * 𝑸 z 𝑸 w
90 89 rspceeqv * 𝑸 z 𝑸 w B w = z 𝑸 * 𝑸 z 𝑸 w x B w = z 𝑸 x
91 76 88 90 syl2anc A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z x B w = z 𝑸 x
92 91 3expia A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A v < 𝑸 z x B w = z 𝑸 x
93 92 reximdv A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A z A v < 𝑸 z z A x B w = z 𝑸 x
94 1 reclem2pr A 𝑷 B 𝑷
95 df-mp 𝑷 = y 𝑷 , w 𝑷 u | f y g w u = f 𝑸 g
96 mulclnq f 𝑸 g 𝑸 f 𝑸 g 𝑸
97 95 96 genpelv A 𝑷 B 𝑷 w A 𝑷 B z A x B w = z 𝑸 x
98 94 97 mpdan A 𝑷 w A 𝑷 B z A x B w = z 𝑸 x
99 98 ad2antrr A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A w A 𝑷 B z A x B w = z 𝑸 x
100 93 99 sylibrd A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A z A v < 𝑸 z w A 𝑷 B
101 18 100 mpd A 𝑷 w < 𝑸 1 𝑸 v A ¬ v 𝑸 * 𝑸 w A w A 𝑷 B
102 16 101 rexlimddv A 𝑷 w < 𝑸 1 𝑸 w A 𝑷 B
103 102 ex A 𝑷 w < 𝑸 1 𝑸 w A 𝑷 B
104 3 103 syl5bi A 𝑷 w 1 𝑷 w A 𝑷 B
105 104 ssrdv A 𝑷 1 𝑷 A 𝑷 B