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