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 sselid ( ( ( ( ( ( 𝐽 = ( 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 sselid ( ( ( ( 𝐽 = ( 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 ) 𝑋 = 𝑏 ) ) )