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 ) ¬ 𝑋 = 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢𝑣 )