Metamath Proof Explorer


Theorem alexsubALTlem3

Description: Lemma for alexsubALT . If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010) (Revised by Mario Carneiro, 14-Dec-2013)

Ref Expression
Hypothesis alexsubALT.1 𝑋 = 𝐽
Assertion alexsubALTlem3 ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 ) ) ) ∧ 𝑤𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ) → ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 )

Proof

Step Hyp Ref Expression
1 alexsubALT.1 𝑋 = 𝐽
2 dfrex2 ( ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = 𝑛 ↔ ¬ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 )
3 2 ralbii ( ∀ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = 𝑛 ↔ ∀ 𝑠𝑡 ¬ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 )
4 ralnex ( ∀ 𝑠𝑡 ¬ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 ↔ ¬ ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 )
5 3 4 bitr2i ( ¬ ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 ↔ ∀ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = 𝑛 )
6 elin ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ↔ ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) )
7 elpwi ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) → 𝑛 ⊆ ( 𝑢 ∪ { 𝑠 } ) )
8 7 adantr ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → 𝑛 ⊆ ( 𝑢 ∪ { 𝑠 } ) )
9 uncom ( 𝑢 ∪ { 𝑠 } ) = ( { 𝑠 } ∪ 𝑢 )
10 8 9 sseqtrdi ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → 𝑛 ⊆ ( { 𝑠 } ∪ 𝑢 ) )
11 ssundif ( 𝑛 ⊆ ( { 𝑠 } ∪ 𝑢 ) ↔ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 )
12 10 11 sylib ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 )
13 diffi ( 𝑛 ∈ Fin → ( 𝑛 ∖ { 𝑠 } ) ∈ Fin )
14 13 adantl ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → ( 𝑛 ∖ { 𝑠 } ) ∈ Fin )
15 12 14 jca ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) )
16 6 15 sylbi ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) )
17 16 adantr ( ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) )
18 17 ad2antll ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) )
19 elin ( ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ( 𝑛 ∖ { 𝑠 } ) ∈ 𝒫 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) )
20 vex 𝑢 ∈ V
21 20 elpw2 ( ( 𝑛 ∖ { 𝑠 } ) ∈ 𝒫 𝑢 ↔ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 )
22 21 anbi1i ( ( ( 𝑛 ∖ { 𝑠 } ) ∈ 𝒫 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ↔ ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) )
23 19 22 bitr2i ( ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ↔ ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) )
24 18 23 sylib ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) )
25 simprrr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑋 = 𝑛 )
26 eldif ( 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ↔ ( 𝑥𝑛 ∧ ¬ 𝑥 ∈ { 𝑠 } ) )
27 26 simplbi2 ( 𝑥𝑛 → ( ¬ 𝑥 ∈ { 𝑠 } → 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) )
28 elun ( 𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ↔ ( 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ∨ 𝑥 ∈ { 𝑠 } ) )
29 orcom ( ( 𝑥 ∈ { 𝑠 } ∨ 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ↔ ( 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ∨ 𝑥 ∈ { 𝑠 } ) )
30 28 29 bitr4i ( 𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ↔ ( 𝑥 ∈ { 𝑠 } ∨ 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) )
31 df-or ( ( 𝑥 ∈ { 𝑠 } ∨ 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ↔ ( ¬ 𝑥 ∈ { 𝑠 } → 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) )
32 30 31 bitr2i ( ( ¬ 𝑥 ∈ { 𝑠 } → 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ↔ 𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) )
33 27 32 sylib ( 𝑥𝑛𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) )
34 33 ssriv 𝑛 ⊆ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } )
35 uniss ( 𝑛 ⊆ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) → 𝑛 ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) )
36 34 35 mp1i ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑛 ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) )
37 uniun ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) = ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } )
38 unisnv { 𝑠 } = 𝑠
39 38 uneq2i ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) = ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 )
40 37 39 eqtri ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) = ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 )
41 36 40 sseqtrdi ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑛 ⊆ ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) )
42 25 41 eqsstrd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑋 ⊆ ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) )
43 difss ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑛
44 43 unissi ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑛
45 sseq2 ( 𝑋 = 𝑛 → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑛 ) )
46 44 45 mpbiri ( 𝑋 = 𝑛 ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 )
47 46 adantl ( ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) → ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 )
48 47 ad2antll ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 )
49 elinel1 ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ∈ 𝒫 𝑥 )
50 49 elpwid ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡𝑥 )
51 50 ad3antrrr ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) → 𝑡𝑥 )
52 51 ad2antlr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑡𝑥 )
53 simprl ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑠𝑡 )
54 52 53 sseldd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑠𝑥 )
55 elssuni ( 𝑠𝑥𝑠 𝑥 )
56 54 55 syl ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑠 𝑥 )
57 fibas ( fi ‘ 𝑥 ) ∈ TopBases
58 unitg ( ( fi ‘ 𝑥 ) ∈ TopBases → ( topGen ‘ ( fi ‘ 𝑥 ) ) = ( fi ‘ 𝑥 ) )
59 57 58 mp1i ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → ( topGen ‘ ( fi ‘ 𝑥 ) ) = ( fi ‘ 𝑥 ) )
60 unieq ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) )
61 60 3ad2ant1 ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) )
62 61 ad3antrrr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) )
63 vex 𝑥 ∈ V
64 fiuni ( 𝑥 ∈ V → 𝑥 = ( fi ‘ 𝑥 ) )
65 63 64 mp1i ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑥 = ( fi ‘ 𝑥 ) )
66 59 62 65 3eqtr4rd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑥 = 𝐽 )
67 66 1 eqtr4di ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑥 = 𝑋 )
68 56 67 sseqtrd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑠𝑋 )
69 48 68 unssd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ⊆ 𝑋 )
70 42 69 eqssd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → 𝑋 = ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) )
71 unieq ( 𝑚 = ( 𝑛 ∖ { 𝑠 } ) → 𝑚 = ( 𝑛 ∖ { 𝑠 } ) )
72 71 uneq1d ( 𝑚 = ( 𝑛 ∖ { 𝑠 } ) → ( 𝑚𝑠 ) = ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) )
73 72 rspceeqv ( ( ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑋 = ( ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ) → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) )
74 24 70 73 syl2anc ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑠𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) ) ) → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) )
75 74 expr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ 𝑠𝑡 ) → ( ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = 𝑛 ) → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) ) )
76 75 expd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ 𝑠𝑡 ) → ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) → ( 𝑋 = 𝑛 → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) ) ) )
77 76 rexlimdv ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ 𝑠𝑡 ) → ( ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = 𝑛 → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) ) )
78 77 ralimdva ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ∀ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = 𝑛 → ∀ 𝑠𝑡𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) ) )
79 elinel2 ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ∈ Fin )
80 79 adantr ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) → 𝑡 ∈ Fin )
81 unieq ( 𝑚 = ( 𝑓𝑠 ) → 𝑚 = ( 𝑓𝑠 ) )
82 81 uneq1d ( 𝑚 = ( 𝑓𝑠 ) → ( 𝑚𝑠 ) = ( ( 𝑓𝑠 ) ∪ 𝑠 ) )
83 82 eqeq2d ( 𝑚 = ( 𝑓𝑠 ) → ( 𝑋 = ( 𝑚𝑠 ) ↔ 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) )
84 83 ac6sfi ( ( 𝑡 ∈ Fin ∧ ∀ 𝑠𝑡𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) )
85 84 ex ( 𝑡 ∈ Fin → ( ∀ 𝑠𝑡𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) )
86 80 85 syl ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) → ( ∀ 𝑠𝑡𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) )
87 86 adantr ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) → ( ∀ 𝑠𝑡𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) )
88 87 ad2antrl ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ∀ 𝑠𝑡𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( 𝑚𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) )
89 ffvelcdm ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑠𝑡 ) → ( 𝑓𝑠 ) ∈ ( 𝒫 𝑢 ∩ Fin ) )
90 elin ( ( 𝑓𝑠 ) ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ( 𝑓𝑠 ) ∈ 𝒫 𝑢 ∧ ( 𝑓𝑠 ) ∈ Fin ) )
91 elpwi ( ( 𝑓𝑠 ) ∈ 𝒫 𝑢 → ( 𝑓𝑠 ) ⊆ 𝑢 )
92 91 adantr ( ( ( 𝑓𝑠 ) ∈ 𝒫 𝑢 ∧ ( 𝑓𝑠 ) ∈ Fin ) → ( 𝑓𝑠 ) ⊆ 𝑢 )
93 90 92 sylbi ( ( 𝑓𝑠 ) ∈ ( 𝒫 𝑢 ∩ Fin ) → ( 𝑓𝑠 ) ⊆ 𝑢 )
94 89 93 syl ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑠𝑡 ) → ( 𝑓𝑠 ) ⊆ 𝑢 )
95 94 ralrimiva ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) → ∀ 𝑠𝑡 ( 𝑓𝑠 ) ⊆ 𝑢 )
96 iunss ( 𝑠𝑡 ( 𝑓𝑠 ) ⊆ 𝑢 ↔ ∀ 𝑠𝑡 ( 𝑓𝑠 ) ⊆ 𝑢 )
97 95 96 sylibr ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) → 𝑠𝑡 ( 𝑓𝑠 ) ⊆ 𝑢 )
98 97 ad2antrl ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑠𝑡 ( 𝑓𝑠 ) ⊆ 𝑢 )
99 simplrr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑤𝑢 )
100 99 snssd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → { 𝑤 } ⊆ 𝑢 )
101 98 100 unssd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 )
102 89 elin2d ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑠𝑡 ) → ( 𝑓𝑠 ) ∈ Fin )
103 102 ralrimiva ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) → ∀ 𝑠𝑡 ( 𝑓𝑠 ) ∈ Fin )
104 iunfi ( ( 𝑡 ∈ Fin ∧ ∀ 𝑠𝑡 ( 𝑓𝑠 ) ∈ Fin ) → 𝑠𝑡 ( 𝑓𝑠 ) ∈ Fin )
105 80 103 104 syl2an ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ) → 𝑠𝑡 ( 𝑓𝑠 ) ∈ Fin )
106 105 ad4ant14 ( ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ∧ 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ) → 𝑠𝑡 ( 𝑓𝑠 ) ∈ Fin )
107 106 ad2ant2lr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑠𝑡 ( 𝑓𝑠 ) ∈ Fin )
108 snfi { 𝑤 } ∈ Fin
109 unfi ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∈ Fin ∧ { 𝑤 } ∈ Fin ) → ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ Fin )
110 107 108 109 sylancl ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ Fin )
111 101 110 jca ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ∧ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) )
112 elin ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) )
113 20 elpw2 ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ 𝒫 𝑢 ↔ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 )
114 113 anbi1i ( ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ 𝒫 𝑢 ∧ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) ↔ ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ∧ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) )
115 112 114 bitr2i ( ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ∧ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) ↔ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) )
116 111 115 sylib ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) )
117 ralnex ( ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ↔ ¬ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) )
118 117 imbi2i ( ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) ↔ ( 𝑣𝑦 → ¬ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) )
119 118 albii ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) ↔ ∀ 𝑦 ( 𝑣𝑦 → ¬ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) )
120 alinexa ( ∀ 𝑦 ( 𝑣𝑦 → ¬ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) ↔ ¬ ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) )
121 119 120 bitr2i ( ¬ ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) ↔ ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) )
122 fveq2 ( 𝑠 = 𝑧 → ( 𝑓𝑠 ) = ( 𝑓𝑧 ) )
123 122 unieqd ( 𝑠 = 𝑧 ( 𝑓𝑠 ) = ( 𝑓𝑧 ) )
124 id ( 𝑠 = 𝑧𝑠 = 𝑧 )
125 123 124 uneq12d ( 𝑠 = 𝑧 → ( ( 𝑓𝑠 ) ∪ 𝑠 ) = ( ( 𝑓𝑧 ) ∪ 𝑧 ) )
126 125 eqeq2d ( 𝑠 = 𝑧 → ( 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ↔ 𝑋 = ( ( 𝑓𝑧 ) ∪ 𝑧 ) ) )
127 126 rspcv ( 𝑧𝑡 → ( ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → 𝑋 = ( ( 𝑓𝑧 ) ∪ 𝑧 ) ) )
128 eleq2 ( 𝑋 = ( ( 𝑓𝑧 ) ∪ 𝑧 ) → ( 𝑣𝑋𝑣 ∈ ( ( 𝑓𝑧 ) ∪ 𝑧 ) ) )
129 128 biimpd ( 𝑋 = ( ( 𝑓𝑧 ) ∪ 𝑧 ) → ( 𝑣𝑋𝑣 ∈ ( ( 𝑓𝑧 ) ∪ 𝑧 ) ) )
130 elun ( 𝑣 ∈ ( ( 𝑓𝑧 ) ∪ 𝑧 ) ↔ ( 𝑣 ( 𝑓𝑧 ) ∨ 𝑣𝑧 ) )
131 eluni ( 𝑣 ( 𝑓𝑧 ) ↔ ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑓𝑧 ) ) )
132 131 orbi1i ( ( 𝑣 ( 𝑓𝑧 ) ∨ 𝑣𝑧 ) ↔ ( ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑓𝑧 ) ) ∨ 𝑣𝑧 ) )
133 df-or ( ( ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑓𝑧 ) ) ∨ 𝑣𝑧 ) ↔ ( ¬ ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑓𝑧 ) ) → 𝑣𝑧 ) )
134 alinexa ( ∀ 𝑤 ( 𝑣𝑤 → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) ↔ ¬ ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑓𝑧 ) ) )
135 134 imbi1i ( ( ∀ 𝑤 ( 𝑣𝑤 → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) → 𝑣𝑧 ) ↔ ( ¬ ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑓𝑧 ) ) → 𝑣𝑧 ) )
136 133 135 bitr4i ( ( ∃ 𝑤 ( 𝑣𝑤𝑤 ∈ ( 𝑓𝑧 ) ) ∨ 𝑣𝑧 ) ↔ ( ∀ 𝑤 ( 𝑣𝑤 → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) → 𝑣𝑧 ) )
137 130 132 136 3bitri ( 𝑣 ∈ ( ( 𝑓𝑧 ) ∪ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑣𝑤 → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) → 𝑣𝑧 ) )
138 eleq2 ( 𝑦 = 𝑤 → ( 𝑣𝑦𝑣𝑤 ) )
139 eleq1w ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 𝑓𝑠 ) ↔ 𝑤 ∈ ( 𝑓𝑠 ) ) )
140 139 notbid ( 𝑦 = 𝑤 → ( ¬ 𝑦 ∈ ( 𝑓𝑠 ) ↔ ¬ 𝑤 ∈ ( 𝑓𝑠 ) ) )
141 140 ralbidv ( 𝑦 = 𝑤 → ( ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ↔ ∀ 𝑠𝑡 ¬ 𝑤 ∈ ( 𝑓𝑠 ) ) )
142 138 141 imbi12d ( 𝑦 = 𝑤 → ( ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) ↔ ( 𝑣𝑤 → ∀ 𝑠𝑡 ¬ 𝑤 ∈ ( 𝑓𝑠 ) ) ) )
143 142 spvv ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → ( 𝑣𝑤 → ∀ 𝑠𝑡 ¬ 𝑤 ∈ ( 𝑓𝑠 ) ) )
144 122 eleq2d ( 𝑠 = 𝑧 → ( 𝑤 ∈ ( 𝑓𝑠 ) ↔ 𝑤 ∈ ( 𝑓𝑧 ) ) )
145 144 notbid ( 𝑠 = 𝑧 → ( ¬ 𝑤 ∈ ( 𝑓𝑠 ) ↔ ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) )
146 145 rspcv ( 𝑧𝑡 → ( ∀ 𝑠𝑡 ¬ 𝑤 ∈ ( 𝑓𝑠 ) → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) )
147 143 146 syl9r ( 𝑧𝑡 → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → ( 𝑣𝑤 → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) ) )
148 147 alrimdv ( 𝑧𝑡 → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → ∀ 𝑤 ( 𝑣𝑤 → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) ) )
149 148 imim1d ( 𝑧𝑡 → ( ( ∀ 𝑤 ( 𝑣𝑤 → ¬ 𝑤 ∈ ( 𝑓𝑧 ) ) → 𝑣𝑧 ) → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑧 ) ) )
150 137 149 biimtrid ( 𝑧𝑡 → ( 𝑣 ∈ ( ( 𝑓𝑧 ) ∪ 𝑧 ) → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑧 ) ) )
151 150 a1dd ( 𝑧𝑡 → ( 𝑣 ∈ ( ( 𝑓𝑧 ) ∪ 𝑧 ) → ( 𝑤 = 𝑡 → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑧 ) ) ) )
152 129 151 syl9r ( 𝑧𝑡 → ( 𝑋 = ( ( 𝑓𝑧 ) ∪ 𝑧 ) → ( 𝑣𝑋 → ( 𝑤 = 𝑡 → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑧 ) ) ) ) )
153 127 152 syld ( 𝑧𝑡 → ( ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → ( 𝑣𝑋 → ( 𝑤 = 𝑡 → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑧 ) ) ) ) )
154 153 com14 ( 𝑤 = 𝑡 → ( ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → ( 𝑣𝑋 → ( 𝑧𝑡 → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑧 ) ) ) ) )
155 154 imp31 ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( 𝑧𝑡 → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑧 ) ) )
156 155 com23 ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → ( 𝑧𝑡𝑣𝑧 ) ) )
157 156 ralrimdv ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → ∀ 𝑧𝑡 𝑣𝑧 ) )
158 vex 𝑣 ∈ V
159 158 elint2 ( 𝑣 𝑡 ↔ ∀ 𝑧𝑡 𝑣𝑧 )
160 157 159 syl6ibr ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣 𝑡 ) )
161 eleq2 ( 𝑤 = 𝑡 → ( 𝑣𝑤𝑣 𝑡 ) )
162 161 ad2antrr ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( 𝑣𝑤𝑣 𝑡 ) )
163 160 162 sylibrd ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( ∀ 𝑦 ( 𝑣𝑦 → ∀ 𝑠𝑡 ¬ 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑤 ) )
164 121 163 biimtrid ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( ¬ ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) → 𝑣𝑤 ) )
165 164 orrd ( ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣𝑋 ) → ( ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) ∨ 𝑣𝑤 ) )
166 165 ex ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) → ( 𝑣𝑋 → ( ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) ∨ 𝑣𝑤 ) ) )
167 orc ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) → ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) )
168 167 anim2i ( ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) → ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
169 168 eximi ( ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) → ∃ 𝑦 ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
170 equid 𝑤 = 𝑤
171 vex 𝑤 ∈ V
172 equequ1 ( 𝑦 = 𝑤 → ( 𝑦 = 𝑤𝑤 = 𝑤 ) )
173 138 172 anbi12d ( 𝑦 = 𝑤 → ( ( 𝑣𝑦𝑦 = 𝑤 ) ↔ ( 𝑣𝑤𝑤 = 𝑤 ) ) )
174 171 173 spcev ( ( 𝑣𝑤𝑤 = 𝑤 ) → ∃ 𝑦 ( 𝑣𝑦𝑦 = 𝑤 ) )
175 170 174 mpan2 ( 𝑣𝑤 → ∃ 𝑦 ( 𝑣𝑦𝑦 = 𝑤 ) )
176 olc ( 𝑦 = 𝑤 → ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) )
177 176 anim2i ( ( 𝑣𝑦𝑦 = 𝑤 ) → ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
178 177 eximi ( ∃ 𝑦 ( 𝑣𝑦𝑦 = 𝑤 ) → ∃ 𝑦 ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
179 175 178 syl ( 𝑣𝑤 → ∃ 𝑦 ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
180 169 179 jaoi ( ( ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) ∨ 𝑣𝑤 ) → ∃ 𝑦 ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
181 eluni ( 𝑣 ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ↔ ∃ 𝑦 ( 𝑣𝑦𝑦 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ) )
182 elun ( 𝑦 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ↔ ( 𝑦 𝑠𝑡 ( 𝑓𝑠 ) ∨ 𝑦 ∈ { 𝑤 } ) )
183 eliun ( 𝑦 𝑠𝑡 ( 𝑓𝑠 ) ↔ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) )
184 velsn ( 𝑦 ∈ { 𝑤 } ↔ 𝑦 = 𝑤 )
185 183 184 orbi12i ( ( 𝑦 𝑠𝑡 ( 𝑓𝑠 ) ∨ 𝑦 ∈ { 𝑤 } ) ↔ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) )
186 182 185 bitri ( 𝑦 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ↔ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) )
187 186 anbi2i ( ( 𝑣𝑦𝑦 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ) ↔ ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
188 187 exbii ( ∃ 𝑦 ( 𝑣𝑦𝑦 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ) ↔ ∃ 𝑦 ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) )
189 181 188 bitr2i ( ∃ 𝑦 ( 𝑣𝑦 ∧ ( ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ∨ 𝑦 = 𝑤 ) ) ↔ 𝑣 ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) )
190 180 189 sylib ( ( ∃ 𝑦 ( 𝑣𝑦 ∧ ∃ 𝑠𝑡 𝑦 ∈ ( 𝑓𝑠 ) ) ∨ 𝑣𝑤 ) → 𝑣 ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) )
191 166 190 syl6 ( ( 𝑤 = 𝑡 ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) → ( 𝑣𝑋𝑣 ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ) )
192 191 ad5ant25 ( ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) → ( 𝑣𝑋𝑣 ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ) )
193 192 ad2ant2l ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑣𝑋𝑣 ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ) )
194 193 ssrdv ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑋 ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) )
195 elun ( 𝑣 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ↔ ( 𝑣 𝑠𝑡 ( 𝑓𝑠 ) ∨ 𝑣 ∈ { 𝑤 } ) )
196 eliun ( 𝑣 𝑠𝑡 ( 𝑓𝑠 ) ↔ ∃ 𝑠𝑡 𝑣 ∈ ( 𝑓𝑠 ) )
197 velsn ( 𝑣 ∈ { 𝑤 } ↔ 𝑣 = 𝑤 )
198 196 197 orbi12i ( ( 𝑣 𝑠𝑡 ( 𝑓𝑠 ) ∨ 𝑣 ∈ { 𝑤 } ) ↔ ( ∃ 𝑠𝑡 𝑣 ∈ ( 𝑓𝑠 ) ∨ 𝑣 = 𝑤 ) )
199 195 198 bitri ( 𝑣 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ↔ ( ∃ 𝑠𝑡 𝑣 ∈ ( 𝑓𝑠 ) ∨ 𝑣 = 𝑤 ) )
200 nfra1 𝑠𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 )
201 nfv 𝑠 𝑣𝑋
202 rsp ( ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → ( 𝑠𝑡𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) )
203 eqimss2 ( 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → ( ( 𝑓𝑠 ) ∪ 𝑠 ) ⊆ 𝑋 )
204 elssuni ( 𝑣 ∈ ( 𝑓𝑠 ) → 𝑣 ( 𝑓𝑠 ) )
205 ssun3 ( 𝑣 ( 𝑓𝑠 ) → 𝑣 ⊆ ( ( 𝑓𝑠 ) ∪ 𝑠 ) )
206 204 205 syl ( 𝑣 ∈ ( 𝑓𝑠 ) → 𝑣 ⊆ ( ( 𝑓𝑠 ) ∪ 𝑠 ) )
207 sstr ( ( 𝑣 ⊆ ( ( 𝑓𝑠 ) ∪ 𝑠 ) ∧ ( ( 𝑓𝑠 ) ∪ 𝑠 ) ⊆ 𝑋 ) → 𝑣𝑋 )
208 207 expcom ( ( ( 𝑓𝑠 ) ∪ 𝑠 ) ⊆ 𝑋 → ( 𝑣 ⊆ ( ( 𝑓𝑠 ) ∪ 𝑠 ) → 𝑣𝑋 ) )
209 203 206 208 syl2im ( 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → ( 𝑣 ∈ ( 𝑓𝑠 ) → 𝑣𝑋 ) )
210 202 209 syl6 ( ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → ( 𝑠𝑡 → ( 𝑣 ∈ ( 𝑓𝑠 ) → 𝑣𝑋 ) ) )
211 200 201 210 rexlimd ( ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) → ( ∃ 𝑠𝑡 𝑣 ∈ ( 𝑓𝑠 ) → 𝑣𝑋 ) )
212 211 ad2antll ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( ∃ 𝑠𝑡 𝑣 ∈ ( 𝑓𝑠 ) → 𝑣𝑋 ) )
213 elpwi ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) )
214 213 ad2antrl ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) )
215 214 ad2antrr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) )
216 215 99 sseldd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑤 ∈ ( fi ‘ 𝑥 ) )
217 elssuni ( 𝑤 ∈ ( fi ‘ 𝑥 ) → 𝑤 ( fi ‘ 𝑥 ) )
218 216 217 syl ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑤 ( fi ‘ 𝑥 ) )
219 57 58 ax-mp ( topGen ‘ ( fi ‘ 𝑥 ) ) = ( fi ‘ 𝑥 )
220 60 219 eqtr2di ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( fi ‘ 𝑥 ) = 𝐽 )
221 220 1 eqtr4di ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( fi ‘ 𝑥 ) = 𝑋 )
222 221 3ad2ant1 ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( fi ‘ 𝑥 ) = 𝑋 )
223 222 ad3antrrr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( fi ‘ 𝑥 ) = 𝑋 )
224 218 223 sseqtrd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑤𝑋 )
225 sseq1 ( 𝑣 = 𝑤 → ( 𝑣𝑋𝑤𝑋 ) )
226 224 225 syl5ibrcom ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑣 = 𝑤𝑣𝑋 ) )
227 212 226 jaod ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( ( ∃ 𝑠𝑡 𝑣 ∈ ( 𝑓𝑠 ) ∨ 𝑣 = 𝑤 ) → 𝑣𝑋 ) )
228 199 227 biimtrid ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑣 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) → 𝑣𝑋 ) )
229 228 ralrimiv ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ∀ 𝑣 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) 𝑣𝑋 )
230 unissb ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑋 ↔ ∀ 𝑣 ∈ ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) 𝑣𝑋 )
231 229 230 sylibr ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑋 )
232 194 231 eqssd ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → 𝑋 = ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) )
233 unieq ( 𝑏 = ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) → 𝑏 = ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) )
234 233 rspceeqv ( ( ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑋 = ( 𝑠𝑡 ( 𝑓𝑠 ) ∪ { 𝑤 } ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = 𝑏 )
235 116 232 234 syl2anc ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = 𝑏 )
236 235 ex ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = 𝑏 ) )
237 236 exlimdv ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠𝑡 𝑋 = ( ( 𝑓𝑠 ) ∪ 𝑠 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = 𝑏 ) )
238 78 88 237 3syld ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ∀ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = 𝑛 → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = 𝑏 ) )
239 5 238 biimtrid ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ¬ ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = 𝑏 ) )
240 dfrex2 ( ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = 𝑏 ↔ ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 )
241 239 240 imbitrdi ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ¬ ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 → ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 ) )
242 241 con4d ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ∧ 𝑤𝑢 ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 → ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 ) )
243 242 exp32 ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) → ( 𝑤𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 → ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 ) ) ) )
244 243 com24 ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎𝑢 ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 → ( 𝑤𝑢 → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) → ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 ) ) ) )
245 244 exp32 ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → ( 𝑎𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 → ( 𝑤𝑢 → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) → ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 ) ) ) ) ) )
246 245 imp45 ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 ) ) ) → ( 𝑤𝑢 → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) → ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 ) ) )
247 246 imp31 ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = 𝑏 ) ) ) ∧ 𝑤𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = 𝑡 ) ∧ ( 𝑦𝑤 ∧ ¬ 𝑦 ( 𝑥𝑢 ) ) ) ) → ∃ 𝑠𝑡𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = 𝑛 )