Metamath Proof Explorer


Theorem alexsubALTlem2

Description: Lemma for alexsubALT . Every subset of a base which has no finite subcover is a subset of a maximal such collection. (Contributed by Jeff Hankins, 27-Jan-2010)

Ref Expression
Hypothesis alexsubALT.1 X = J
Assertion alexsubALTlem2 J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b u z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b v z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b ¬ u v

Proof

Step Hyp Ref Expression
1 alexsubALT.1 X = J
2 ssel y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w y w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
3 elun w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w
4 sseq2 z = w a z a w
5 pweq z = w 𝒫 z = 𝒫 w
6 5 ineq1d z = w 𝒫 z Fin = 𝒫 w Fin
7 6 raleqdv z = w b 𝒫 z Fin ¬ X = b b 𝒫 w Fin ¬ X = b
8 4 7 anbi12d z = w a z b 𝒫 z Fin ¬ X = b a w b 𝒫 w Fin ¬ X = b
9 8 elrab w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b
10 velsn w w =
11 9 10 orbi12i w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b w =
12 3 11 bitri w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b w =
13 elpwi w 𝒫 fi x w fi x
14 13 adantr w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b w fi x
15 0ss fi x
16 sseq1 w = w fi x fi x
17 15 16 mpbiri w = w fi x
18 14 17 jaoi w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b w = w fi x
19 12 18 sylbi w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w fi x
20 2 19 syl6 y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w y w fi x
21 20 ralrimiv y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w y w fi x
22 unissb y fi x w y w fi x
23 21 22 sylibr y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y fi x
24 23 adantr y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y y fi x
25 24 ad2antlr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = y fi x
26 vuniex y V
27 26 elpw y 𝒫 fi x y fi x
28 25 27 sylibr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = y 𝒫 fi x
29 uni0b y = y
30 29 notbii ¬ y = ¬ y
31 disjssun y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b = y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y
32 31 biimpcd y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b = y
33 32 necon3bd y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b ¬ y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
34 n0 y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w w y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
35 elin w y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w y w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
36 9 anbi2i w y w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w y w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b
37 35 36 bitri w y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w y w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b
38 simprrl w y w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b a w
39 simpl w y w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b w y
40 ssuni a w w y a y
41 38 39 40 syl2anc w y w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b a y
42 37 41 sylbi w y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b a y
43 42 exlimiv w w y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b a y
44 34 43 sylbi y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b a y
45 33 44 syl6 y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b ¬ y a y
46 45 ad2antrl J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y a y
47 30 46 syl5bi J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = a y
48 47 imp J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = a y
49 elfpw n 𝒫 y Fin n y n Fin
50 unieq y = y =
51 uni0 =
52 50 51 eqtrdi y = y =
53 52 necon3bi ¬ y = y
54 53 adantr ¬ y = n Fin y
55 54 ad2antrl J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y y
56 simplrr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y [⊂] Or y
57 simprlr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y n Fin
58 simprr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y n y
59 finsschain y [⊂] Or y n Fin n y w y n w
60 55 56 57 58 59 syl22anc J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y w y n w
61 60 expr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y w y n w
62 0elpw 𝒫 a
63 0fin Fin
64 62 63 elini 𝒫 a Fin
65 unieq b = b =
66 65 eqeq2d b = X = b X =
67 66 notbid b = ¬ X = b ¬ X =
68 67 rspccv b 𝒫 a Fin ¬ X = b 𝒫 a Fin ¬ X =
69 64 68 mpi b 𝒫 a Fin ¬ X = b ¬ X =
70 velpw n 𝒫 w n w
71 elin n 𝒫 w Fin n 𝒫 w n Fin
72 unieq b = n b = n
73 72 eqeq2d b = n X = b X = n
74 73 notbid b = n ¬ X = b ¬ X = n
75 74 rspccv b 𝒫 w Fin ¬ X = b n 𝒫 w Fin ¬ X = n
76 71 75 syl5bir b 𝒫 w Fin ¬ X = b n 𝒫 w n Fin ¬ X = n
77 76 expd b 𝒫 w Fin ¬ X = b n 𝒫 w n Fin ¬ X = n
78 70 77 syl5bir b 𝒫 w Fin ¬ X = b n w n Fin ¬ X = n
79 78 com23 b 𝒫 w Fin ¬ X = b n Fin n w ¬ X = n
80 79 ad2antll w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b n Fin n w ¬ X = n
81 80 a1i ¬ X = w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b n Fin n w ¬ X = n
82 sseq2 w = n w n
83 ss0 n n =
84 82 83 syl6bi w = n w n =
85 unieq n = n =
86 85 eqeq2d n = X = n X =
87 86 notbid n = ¬ X = n ¬ X =
88 87 biimprcd ¬ X = n = ¬ X = n
89 88 a1dd ¬ X = n = n Fin ¬ X = n
90 84 89 syl9r ¬ X = w = n w n Fin ¬ X = n
91 90 com34 ¬ X = w = n Fin n w ¬ X = n
92 81 91 jaod ¬ X = w 𝒫 fi x a w b 𝒫 w Fin ¬ X = b w = n Fin n w ¬ X = n
93 12 92 syl5bi ¬ X = w z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b n Fin n w ¬ X = n
94 2 93 sylan9r ¬ X = y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b w y n Fin n w ¬ X = n
95 94 com23 ¬ X = y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b n Fin w y n w ¬ X = n
96 69 95 sylan b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b n Fin w y n w ¬ X = n
97 96 ad2ant2lr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y n Fin w y n w ¬ X = n
98 97 imp J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y n Fin w y n w ¬ X = n
99 98 adantrl J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin w y n w ¬ X = n
100 99 rexlimdv J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin w y n w ¬ X = n
101 61 100 syld J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y ¬ X = n
102 101 expr J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n Fin n y ¬ X = n
103 102 impcomd J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n y n Fin ¬ X = n
104 49 103 syl5bi J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n 𝒫 y Fin ¬ X = n
105 104 ralrimiv J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = n 𝒫 y Fin ¬ X = n
106 unieq n = b n = b
107 106 eqeq2d n = b X = n X = b
108 107 notbid n = b ¬ X = n ¬ X = b
109 108 cbvralvw n 𝒫 y Fin ¬ X = n b 𝒫 y Fin ¬ X = b
110 105 109 sylib J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = b 𝒫 y Fin ¬ X = b
111 28 48 110 jca32 J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b
112 111 ex J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y ¬ y = y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b
113 orcom y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y
114 26 elsn y y =
115 sseq2 z = y a z a y
116 pweq z = y 𝒫 z = 𝒫 y
117 116 ineq1d z = y 𝒫 z Fin = 𝒫 y Fin
118 117 raleqdv z = y b 𝒫 z Fin ¬ X = b b 𝒫 y Fin ¬ X = b
119 115 118 anbi12d z = y a z b 𝒫 z Fin ¬ X = b a y b 𝒫 y Fin ¬ X = b
120 119 elrab y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b
121 114 120 orbi12i y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y = y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b
122 df-or y = y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b ¬ y = y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b
123 121 122 bitr2i ¬ y = y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
124 elun y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b y
125 113 123 124 3bitr4i ¬ y = y 𝒫 fi x a y b 𝒫 y Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
126 112 125 sylib J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
127 126 ex J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
128 127 alrimiv J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b
129 fvex fi x V
130 129 pwex 𝒫 fi x V
131 130 rabex z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b V
132 p0ex V
133 131 132 unex z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b V
134 133 zorn y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b [⊂] Or y y z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b u z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b v z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b ¬ u v
135 128 134 syl J = topGen fi x c 𝒫 x X = c d 𝒫 c Fin X = d a 𝒫 fi x b 𝒫 a Fin ¬ X = b u z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b v z 𝒫 fi x | a z b 𝒫 z Fin ¬ X = b ¬ u v