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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃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∈yw⊆fi⁡x
22 unissb ⊢⋃y⊆fi⁡x↔∀w∈yw⊆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∪∅∧[⊂]Ory→⋃y⊆fi⁡x
25 24 ad2antlr ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃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≠∅↔∃ww∈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 ⊢∃ww∈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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→¬y⊆∅→a⊆⋃y
47 30 46 biimtrid ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→¬⋃y=∅→a⊆⋃y
48 47 imp ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin∧n⊆⋃y→y≠∅
56 simplrr ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin∧n⊆⋃y→[⊂]Ory
57 simprlr ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin∧n⊆⋃y→n∈Fin
58 simprr ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin∧n⊆⋃y→n⊆⋃y
59 finsschain ⊢y≠∅∧[⊂]Ory∧n∈Fin∧n⊆⋃y→∃w∈yn⊆w
60 55 56 57 58 59 syl22anc ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin∧n⊆⋃y→∃w∈yn⊆w
61 60 expr ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin→n⊆⋃y→∃w∈yn⊆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 biimtrrid ⊢∀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 biimtrrid ⊢∀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 biimtrid ⊢¬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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→n∈Fin→w∈y→n⊆w→¬X=⋃n
98 97 imp ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧n∈Fin→w∈y→n⊆w→¬X=⋃n
99 98 adantrl ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin→w∈y→n⊆w→¬X=⋃n
100 99 rexlimdv ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin→∃w∈yn⊆w→¬X=⋃n
101 61 100 syld ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅∧n∈Fin→n⊆⋃y→¬X=⋃n
102 101 expr ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅→n∈Fin→n⊆⋃y→¬X=⋃n
103 102 impcomd ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅→n⊆⋃y∧n∈Fin→¬X=⋃n
104 49 103 biimtrid ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅→n∈𝒫⋃y∩Fin→¬X=⋃n
105 104 ralrimiv ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅→∀b∈𝒫⋃y∩Fin¬X=⋃b
111 28 48 110 jca32 ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory∧¬⋃y=∅→⋃y∈𝒫fi⁡x∧a⊆⋃y∧∀b∈𝒫⋃y∩Fin¬X=⋃b
112 111 ex ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→¬⋃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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b∧y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→⋃y∈z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅
127 126 ex ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b→y⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→⋃y∈z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅
128 127 alrimiv ⊢J=topGen⁡fi⁡x∧∀c∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃d∧a∈𝒫fi⁡x∧∀b∈𝒫a∩Fin¬X=⋃b→∀yy⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→⋃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 ⊢∀yy⊆z∈𝒫fi⁡x|a⊆z∧∀b∈𝒫z∩Fin¬X=⋃b∪∅∧[⊂]Ory→⋃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∈𝒫xX=⋃c→∃d∈𝒫c∩FinX=⋃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