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 imbitrrdi ⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ ∩ 𝑡 ) )
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 ) ¬ 𝑋 = ∪ 𝑛 )