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 ⊢ 𝑋 = ∪ 𝐽
Assertion alexsubALTlem2 ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ∃ 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 )

Proof

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