Metamath Proof Explorer

Theorem alexsubALTlem4

Description: Lemma for alexsubALT . If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010) (Revised by Mario Carneiro, 14-Dec-2013)

Ref Expression
Hypothesis alexsubALT.1 ⊢ 𝑋 = ∪ 𝐽
Assertion alexsubALTlem4 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 alexsubALT.1 ⊢ 𝑋 = ∪ 𝐽
2 ralnex ⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ¬ ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 )
3 1 alexsubALTlem2 ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ∃ 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 )
4 elun ⊢ ( 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ ( 𝑢 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ 𝑢 ∈ { ∅ } ) )
5 sseq2 ⊢ ( 𝑧 = 𝑢 → ( 𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑢 ) )
6 pweq ⊢ ( 𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢 )
7 6 ineq1d ⊢ ( 𝑧 = 𝑢 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 𝑢 ∩ Fin ) )
8 7 raleqdv ⊢ ( 𝑧 = 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) )
9 5 8 anbi12d ⊢ ( 𝑧 = 𝑢 → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) )
10 9 elrab ⊢ ( 𝑢 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ↔ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) )
11 velsn ⊢ ( 𝑢 ∈ { ∅ } ↔ 𝑢 = ∅ )
12 10 11 orbi12i ⊢ ( ( 𝑢 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ 𝑢 ∈ { ∅ } ) ↔ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑢 = ∅ ) )
13 4 12 bitri ⊢ ( 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑢 = ∅ ) )
14 ralnex ⊢ ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 )
15 simprrl ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → 𝑎 ⊆ 𝑢 )
16 15 unissd ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ∪ 𝑎 ⊆ ∪ 𝑢 )
17 sseq1 ⊢ ( 𝑋 = ∪ 𝑎 → ( 𝑋 ⊆ ∪ 𝑢 ↔ ∪ 𝑎 ⊆ ∪ 𝑢 ) )
18 16 17 syl5ibrcom ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 = ∪ 𝑎 → 𝑋 ⊆ ∪ 𝑢 ) )
19 vex ⊢ 𝑥 ∈ V
20 inss1 ⊢ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑥
21 19 20 elpwi2 ⊢ ( 𝑥 ∩ 𝑢 ) ∈ 𝒫 𝑥
22 unieq ⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ∪ 𝑐 = ∪ ( 𝑥 ∩ 𝑢 ) )
23 22 eqeq2d ⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( 𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) )
24 pweq ⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → 𝒫 𝑐 = 𝒫 ( 𝑥 ∩ 𝑢 ) )
25 24 ineq1d ⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( 𝒫 𝑐 ∩ Fin ) = ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) )
26 25 rexeqdv ⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ↔ ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
27 23 26 imbi12d ⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ↔ ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
28 27 rspccv ⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( ( 𝑥 ∩ 𝑢 ) ∈ 𝒫 𝑥 → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
29 21 28 mpi ⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
30 inss2 ⊢ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑢
31 sstr ⊢ ( ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) ∧ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑢 ) → 𝑑 ⊆ 𝑢 )
32 30 31 mpan2 ⊢ ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) → 𝑑 ⊆ 𝑢 )
33 32 anim1i ⊢ ( ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) ∧ 𝑑 ∈ Fin ) → ( 𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin ) )
34 elfpw ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) ↔ ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) ∧ 𝑑 ∈ Fin ) )
35 elfpw ⊢ ( 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( 𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin ) )
36 33 34 35 3imtr4i ⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) → 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) )
37 36 anim1i ⊢ ( ( 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑋 = ∪ 𝑑 ) )
38 37 reximi2 ⊢ ( ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 → ∃ 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑑 )
39 29 38 syl6 ⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
40 unieq ⊢ ( 𝑑 = 𝑏 → ∪ 𝑑 = ∪ 𝑏 )
41 40 eqeq2d ⊢ ( 𝑑 = 𝑏 → ( 𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ 𝑏 ) )
42 41 cbvrexvw ⊢ ( ∃ 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑑 ↔ ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 )
43 39 42 syl6ib ⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
44 dfrex2 ⊢ ( ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ↔ ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 )
45 43 44 syl6ib ⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) )
46 45 con2d ⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) )
47 46 a1d ⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑎 ⊆ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) )
48 47 3ad2ant2 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑎 ⊆ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) )
49 48 adantr ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑎 ⊆ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) )
50 49 impd ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) )
51 50 impr ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) )
52 20 unissi ⊢ ∪ ( 𝑥 ∩ 𝑢 ) ⊆ ∪ 𝑥
53 fiuni ⊢ ( 𝑥 ∈ V → ∪ 𝑥 = ∪ ( fi ‘ 𝑥 ) )
54 53 elv ⊢ ∪ 𝑥 = ∪ ( fi ‘ 𝑥 )
55 fibas ⊢ ( fi ‘ 𝑥 ) ∈ TopBases
56 unitg ⊢ ( ( fi ‘ 𝑥 ) ∈ TopBases → ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) = ∪ ( fi ‘ 𝑥 ) )
57 55 56 ax-mp ⊢ ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) = ∪ ( fi ‘ 𝑥 )
58 54 57 eqtr4i ⊢ ∪ 𝑥 = ∪ ( topGen ‘ ( fi ‘ 𝑥 ) )
59 unieq ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ 𝐽 = ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) )
60 58 59 eqtr4id ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ 𝑥 = ∪ 𝐽 )
61 60 1 eqtr4di ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ 𝑥 = 𝑋 )
62 61 3ad2ant1 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ∪ 𝑥 = 𝑋 )
63 62 adantr ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ∪ 𝑥 = 𝑋 )
64 52 63 sseqtrid ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 )
65 eqcom ⊢ ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∪ ( 𝑥 ∩ 𝑢 ) = 𝑋 )
66 eqss ⊢ ( ∪ ( 𝑥 ∩ 𝑢 ) = 𝑋 ↔ ( ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) )
67 66 baib ⊢ ( ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 → ( ∪ ( 𝑥 ∩ 𝑢 ) = 𝑋 ↔ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) )
68 65 67 syl5bb ⊢ ( ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ↔ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) )
69 64 68 syl ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ↔ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) )
70 51 69 mtbid ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ¬ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) )
71 sstr2 ⊢ ( 𝑋 ⊆ ∪ 𝑢 → ( ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) → 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) )
72 71 con3rr3 ⊢ ( ¬ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) → ( 𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) )
73 70 72 syl ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) )
74 nss ⊢ ( ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) )
75 df-rex ⊢ ( ∃ 𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) )
76 74 75 bitr4i ⊢ ( ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∃ 𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) )
77 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝑢 ↔ ∃ 𝑤 ∈ 𝑢 𝑦 ∈ 𝑤 )
78 elpwi ⊢ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) )
79 78 sseld ⊢ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → ( 𝑤 ∈ 𝑢 → 𝑤 ∈ ( fi ‘ 𝑥 ) ) )
80 79 ad2antrl ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → 𝑤 ∈ ( fi ‘ 𝑥 ) ) )
81 elfi ⊢ ( ( 𝑤 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑤 ∈ ( fi ‘ 𝑥 ) ↔ ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 ) )
82 81 el2v ⊢ ( 𝑤 ∈ ( fi ‘ 𝑥 ) ↔ ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 )
83 80 82 syl6ib ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 ) )
84 1 alexsubALTlem3 ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 )
85 78 adantr ⊢ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) )
86 85 ad4antlr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) )
87 ssfii ⊢ ( 𝑥 ∈ V → 𝑥 ⊆ ( fi ‘ 𝑥 ) )
88 87 elv ⊢ 𝑥 ⊆ ( fi ‘ 𝑥 )
89 elinel1 ⊢ ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ∈ 𝒫 𝑥 )
90 89 elpwid ⊢ ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ⊆ 𝑥 )
91 90 ad2antrr ⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) → 𝑡 ⊆ 𝑥 )
92 91 ad2antlr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑡 ⊆ 𝑥 )
93 simprl ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑠 ∈ 𝑡 )
94 92 93 sseldd ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑠 ∈ 𝑥 )
95 88 94 sseldi ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑠 ∈ ( fi ‘ 𝑥 ) )
96 95 snssd ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → { 𝑠 } ⊆ ( fi ‘ 𝑥 ) )
97 86 96 unssd ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ⊆ ( fi ‘ 𝑥 ) )
98 fvex ⊢ ( fi ‘ 𝑥 ) ∈ V
99 98 elpw2 ⊢ ( ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) ↔ ( 𝑢 ∪ { 𝑠 } ) ⊆ ( fi ‘ 𝑥 ) )
100 97 99 sylibr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) )
101 simprl ⊢ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → 𝑎 ⊆ 𝑢 )
102 101 ad4antlr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑎 ⊆ 𝑢 )
103 ssun1 ⊢ 𝑢 ⊆ ( 𝑢 ∪ { 𝑠 } )
104 102 103 sstrdi ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) )
105 unieq ⊢ ( 𝑛 = 𝑏 → ∪ 𝑛 = ∪ 𝑏 )
106 105 eqeq2d ⊢ ( 𝑛 = 𝑏 → ( 𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏 ) )
107 106 notbid ⊢ ( 𝑛 = 𝑏 → ( ¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏 ) )
108 107 cbvralvw ⊢ ( ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ↔ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 )
109 108 biimpi ⊢ ( ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 → ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 )
110 109 ad2antll ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 )
111 100 104 110 jca32 ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) )
112 sseq2 ⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ) )
113 pweq ⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → 𝒫 𝑧 = 𝒫 ( 𝑢 ∪ { 𝑠 } ) )
114 113 ineq1d ⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) )
115 114 raleqdv ⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) )
116 112 115 anbi12d ⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ( 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) )
117 116 elrab ⊢ ( ( 𝑢 ∪ { 𝑠 } ) ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ↔ ( ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) )
118 111 117 sylibr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } )
119 elun1 ⊢ ( ( 𝑢 ∪ { 𝑠 } ) ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } → ( 𝑢 ∪ { 𝑠 } ) ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) )
120 118 119 syl ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) )
121 vsnid ⊢ 𝑠 ∈ { 𝑠 }
122 elun2 ⊢ ( 𝑠 ∈ { 𝑠 } → 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) )
123 121 122 ax-mp ⊢ 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } )
124 intss1 ⊢ ( 𝑠 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑠 )
125 sseq1 ⊢ ( 𝑤 = ∩ 𝑡 → ( 𝑤 ⊆ 𝑠 ↔ ∩ 𝑡 ⊆ 𝑠 ) )
126 124 125 syl5ibrcom ⊢ ( 𝑠 ∈ 𝑡 → ( 𝑤 = ∩ 𝑡 → 𝑤 ⊆ 𝑠 ) )
127 126 impcom ⊢ ( ( 𝑤 = ∩ 𝑡 ∧ 𝑠 ∈ 𝑡 ) → 𝑤 ⊆ 𝑠 )
128 127 ad4ant24 ⊢ ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ 𝑠 ∈ 𝑡 ) → 𝑤 ⊆ 𝑠 )
129 128 adantl ⊢ ( ( 𝑤 ∈ 𝑢 ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ 𝑠 ∈ 𝑡 ) ) → 𝑤 ⊆ 𝑠 )
130 129 adantrrr ⊢ ( ( 𝑤 ∈ 𝑢 ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑤 ⊆ 𝑠 )
131 130 adantll ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑤 ⊆ 𝑠 )
132 simprlr ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑦 ∈ 𝑤 )
133 131 132 sseldd ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑦 ∈ 𝑠 )
134 90 ad2antrr ⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) → 𝑡 ⊆ 𝑥 )
135 134 ad2antrl ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑡 ⊆ 𝑥 )
136 simprrl ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ∈ 𝑡 )
137 135 136 sseldd ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ∈ 𝑥 )
138 elin ⊢ ( 𝑠 ∈ ( 𝑥 ∩ 𝑢 ) ↔ ( 𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢 ) )
139 elunii ⊢ ( ( 𝑦 ∈ 𝑠 ∧ 𝑠 ∈ ( 𝑥 ∩ 𝑢 ) ) → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) )
140 139 ex ⊢ ( 𝑦 ∈ 𝑠 → ( 𝑠 ∈ ( 𝑥 ∩ 𝑢 ) → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) )
141 138 140 syl5bir ⊢ ( 𝑦 ∈ 𝑠 → ( ( 𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢 ) → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) )
142 141 expd ⊢ ( 𝑦 ∈ 𝑠 → ( 𝑠 ∈ 𝑥 → ( 𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) )
143 133 137 142 sylc ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → ( 𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) )
144 143 con3d ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ¬ 𝑠 ∈ 𝑢 ) )
145 144 expr ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ) → ( ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ¬ 𝑠 ∈ 𝑢 ) ) )
146 145 com23 ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ) → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ( ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) → ¬ 𝑠 ∈ 𝑢 ) ) )
147 146 exp32 ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ( ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) → ¬ 𝑠 ∈ 𝑢 ) ) ) ) )
148 147 imp55 ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ¬ 𝑠 ∈ 𝑢 )
149 vex ⊢ 𝑠 ∈ V
150 eleq1w ⊢ ( 𝑣 = 𝑠 → ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ↔ 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) ) )
151 elequ1 ⊢ ( 𝑣 = 𝑠 → ( 𝑣 ∈ 𝑢 ↔ 𝑠 ∈ 𝑢 ) )
152 151 notbid ⊢ ( 𝑣 = 𝑠 → ( ¬ 𝑣 ∈ 𝑢 ↔ ¬ 𝑠 ∈ 𝑢 ) )
153 150 152 anbi12d ⊢ ( 𝑣 = 𝑠 → ( ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) ↔ ( 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑠 ∈ 𝑢 ) ) )
154 149 153 spcev ⊢ ( ( 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑠 ∈ 𝑢 ) → ∃ 𝑣 ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) )
155 123 148 154 sylancr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ∃ 𝑣 ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) )
156 nss ⊢ ( ¬ ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) )
157 155 156 sylibr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ¬ ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 )
158 eqimss2 ⊢ ( 𝑢 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 )
159 158 necon3bi ⊢ ( ¬ ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 → 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) )
160 157 159 syl ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) )
161 160 103 jctil ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) ) )
162 df-pss ⊢ ( 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) ↔ ( 𝑢 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) ) )
163 161 162 sylibr ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) )
164 psseq2 ⊢ ( 𝑣 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) ) )
165 164 rspcev ⊢ ( ( ( 𝑢 ∪ { 𝑠 } ) ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 )
166 120 163 165 syl2anc ⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 )
167 84 166 rexlimddv ⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 )
168 167 exp45 ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) )
169 168 expd ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → ( 𝑤 = ∩ 𝑡 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) ) )
170 169 rexlimdv ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) )
171 170 ex ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → ( ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) ) )
172 83 171 mpdd ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) )
173 172 rexlimdv ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ∃ 𝑤 ∈ 𝑢 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) )
174 77 173 syl5bi ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑦 ∈ ∪ 𝑢 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) )
175 174 rexlimdv ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ∃ 𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) )
176 76 175 syl5bi ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) )
177 18 73 176 3syld ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 = ∪ 𝑎 → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) )
178 177 con3d ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ¬ ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) )
179 14 178 syl5bi ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) )
180 179 ex ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) )
181 180 adantr ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) )
182 ssun1 ⊢ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } )
183 eqimss2 ⊢ ( 𝑧 = 𝑎 → 𝑎 ⊆ 𝑧 )
184 183 biantrurd ⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) )
185 pweq ⊢ ( 𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎 )
186 185 ineq1d ⊢ ( 𝑧 = 𝑎 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 𝑎 ∩ Fin ) )
187 186 raleqdv ⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) )
188 184 187 bitr3d ⊢ ( 𝑧 = 𝑎 → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) )
189 simpll3 ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) )
190 simplr ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 )
191 188 189 190 elrabd ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → 𝑎 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } )
192 182 191 sseldi ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → 𝑎 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) )
193 psseq2 ⊢ ( 𝑣 = 𝑎 → ( 𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ 𝑎 ) )
194 193 notbid ⊢ ( 𝑣 = 𝑎 → ( ¬ 𝑢 ⊊ 𝑣 ↔ ¬ 𝑢 ⊊ 𝑎 ) )
195 194 rspcv ⊢ ( 𝑎 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎 ) )
196 192 195 syl ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎 ) )
197 id ⊢ ( 𝑎 = ∅ → 𝑎 = ∅ )
198 0elpw ⊢ ∅ ∈ 𝒫 𝑎
199 0fin ⊢ ∅ ∈ Fin
200 198 199 elini ⊢ ∅ ∈ ( 𝒫 𝑎 ∩ Fin )
201 197 200 eqeltrdi ⊢ ( 𝑎 = ∅ → 𝑎 ∈ ( 𝒫 𝑎 ∩ Fin ) )
202 unieq ⊢ ( 𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎 )
203 202 eqeq2d ⊢ ( 𝑏 = 𝑎 → ( 𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑎 ) )
204 203 notbid ⊢ ( 𝑏 = 𝑎 → ( ¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑎 ) )
205 204 rspccv ⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑎 ∈ ( 𝒫 𝑎 ∩ Fin ) → ¬ 𝑋 = ∪ 𝑎 ) )
206 201 205 syl5 ⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑎 = ∅ → ¬ 𝑋 = ∪ 𝑎 ) )
207 206 necon2ad ⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅ ) )
208 207 ad2antlr ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅ ) )
209 psseq1 ⊢ ( 𝑢 = ∅ → ( 𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎 ) )
210 209 adantl ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎 ) )
211 0pss ⊢ ( ∅ ⊊ 𝑎 ↔ 𝑎 ≠ ∅ )
212 210 211 bitrdi ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑢 ⊊ 𝑎 ↔ 𝑎 ≠ ∅ ) )
213 208 212 sylibrd ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑋 = ∪ 𝑎 → 𝑢 ⊊ 𝑎 ) )
214 196 213 nsyld ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) )
215 214 ex ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( 𝑢 = ∅ → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) )
216 181 215 jaod ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑢 = ∅ ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) )
217 13 216 syl5bi ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) )
218 217 rexlimdv ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( ∃ 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) )
219 3 218 mpd ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ¬ 𝑋 = ∪ 𝑎 )
220 219 ex ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎 ) )
221 2 220 syl5bir ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ¬ ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎 ) )
222 221 con4d ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
223 222 3exp ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) → ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) )
224 223 ralrimdv ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )