Metamath Proof Explorer

Theorem alexsubALT

Description: The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010) (Revised by Mario Carneiro, 11-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 alexsubALT.1 ⊢ 𝑋 = ∪ 𝐽
2 1 alexsubALTlem1 ⊢ ( 𝐽 ∈ Comp → ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
3 1 alexsubALTlem4 ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
4 velpw ⊢ ( 𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽 )
5 eleq2 ⊢ ( 𝑋 = ∪ 𝑐 → ( 𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐 ) )
6 5 3ad2ant3 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐 ) )
7 eluni ⊢ ( 𝑡 ∈ ∪ 𝑐 ↔ ∃ 𝑤 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐 ) )
8 ssel ⊢ ( 𝑐 ⊆ 𝐽 → ( 𝑤 ∈ 𝑐 → 𝑤 ∈ 𝐽 ) )
9 eleq2 ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( 𝑤 ∈ 𝐽 ↔ 𝑤 ∈ ( topGen ‘ ( fi ‘ 𝑥 ) ) ) )
10 tg2 ⊢ ( ( 𝑤 ∈ ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑡 ∈ 𝑤 ) → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤 ) )
11 10 ex ⊢ ( 𝑤 ∈ ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤 ) ) )
12 9 11 syl6bi ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( 𝑤 ∈ 𝐽 → ( 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤 ) ) ) )
13 8 12 sylan9r ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ) → ( 𝑤 ∈ 𝑐 → ( 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤 ) ) ) )
14 13 3impia ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐 ) → ( 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤 ) ) )
15 sseq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑤 ) )
16 15 rspcev ⊢ ( ( 𝑤 ∈ 𝑐 ∧ 𝑦 ⊆ 𝑤 ) → ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 )
17 16 ex ⊢ ( 𝑤 ∈ 𝑐 → ( 𝑦 ⊆ 𝑤 → ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) )
18 17 3ad2ant3 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐 ) → ( 𝑦 ⊆ 𝑤 → ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) )
19 18 anim2d ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐 ) → ( ( 𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤 ) → ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
20 19 reximdv ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐 ) → ( ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤 ) → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
21 14 20 syld ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐 ) → ( 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
22 21 3expia ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ) → ( 𝑤 ∈ 𝑐 → ( 𝑡 ∈ 𝑤 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) ) )
23 22 com23 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ) → ( 𝑡 ∈ 𝑤 → ( 𝑤 ∈ 𝑐 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) ) )
24 23 impd ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ) → ( ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐 ) → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
25 24 exlimdv ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ) → ( ∃ 𝑤 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐 ) → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
26 7 25 syl5bi ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ) → ( 𝑡 ∈ ∪ 𝑐 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
27 26 3adant3 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑡 ∈ ∪ 𝑐 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
28 6 27 sylbid ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑡 ∈ 𝑋 → ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
29 ssel ⊢ ( 𝑦 ⊆ 𝑧 → ( 𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑧 ) )
30 elunii ⊢ ( ( 𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝑐 ) → 𝑡 ∈ ∪ 𝑐 )
31 30 expcom ⊢ ( 𝑧 ∈ 𝑐 → ( 𝑡 ∈ 𝑧 → 𝑡 ∈ ∪ 𝑐 ) )
32 6 biimprd ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑡 ∈ ∪ 𝑐 → 𝑡 ∈ 𝑋 ) )
33 31 32 sylan9r ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑧 ∈ 𝑐 ) → ( 𝑡 ∈ 𝑧 → 𝑡 ∈ 𝑋 ) )
34 29 33 syl9r ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑧 ∈ 𝑐 ) → ( 𝑦 ⊆ 𝑧 → ( 𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋 ) ) )
35 34 rexlimdva ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → ( 𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋 ) ) )
36 35 com23 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑡 ∈ 𝑦 → ( ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → 𝑡 ∈ 𝑋 ) ) )
37 36 impd ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) → 𝑡 ∈ 𝑋 ) )
38 37 rexlimdvw ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) → 𝑡 ∈ 𝑋 ) )
39 28 38 impbid ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑡 ∈ 𝑋 ↔ ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) ) )
40 elunirab ⊢ ( 𝑡 ∈ ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ↔ ∃ 𝑦 ∈ ( fi ‘ 𝑥 ) ( 𝑡 ∈ 𝑦 ∧ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ) )
41 39 40 bitr4di ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ) )
42 41 eqrdv ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → 𝑋 = ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } )
43 ssrab2 ⊢ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ⊆ ( fi ‘ 𝑥 )
44 fvex ⊢ ( fi ‘ 𝑥 ) ∈ V
45 44 elpw2 ⊢ ( { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∈ 𝒫 ( fi ‘ 𝑥 ) ↔ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ⊆ ( fi ‘ 𝑥 ) )
46 43 45 mpbir ⊢ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∈ 𝒫 ( fi ‘ 𝑥 )
47 unieq ⊢ ( 𝑎 = { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∪ 𝑎 = ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } )
48 47 eqeq2d ⊢ ( 𝑎 = { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( 𝑋 = ∪ 𝑎 ↔ 𝑋 = ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ) )
49 pweq ⊢ ( 𝑎 = { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → 𝒫 𝑎 = 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } )
50 49 ineq1d ⊢ ( 𝑎 = { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( 𝒫 𝑎 ∩ Fin ) = ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) )
51 50 rexeqdv ⊢ ( 𝑎 = { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ↔ ∃ 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
52 48 51 imbi12d ⊢ ( 𝑎 = { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ↔ ( 𝑋 = ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∃ 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
53 52 rspcv ⊢ ( { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∈ 𝒫 ( fi ‘ 𝑥 ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ( 𝑋 = ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∃ 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) )
54 46 53 ax-mp ⊢ ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ( 𝑋 = ∪ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∃ 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
55 42 54 syl5com ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ∃ 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) 𝑋 = ∪ 𝑏 ) )
56 elfpw ⊢ ( 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) ↔ ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∧ 𝑏 ∈ Fin ) )
57 ssel ⊢ ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( 𝑡 ∈ 𝑏 → 𝑡 ∈ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ) )
58 sseq1 ⊢ ( 𝑦 = 𝑡 → ( 𝑦 ⊆ 𝑧 ↔ 𝑡 ⊆ 𝑧 ) )
59 58 rexbidv ⊢ ( 𝑦 = 𝑡 → ( ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ↔ ∃ 𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 ) )
60 59 elrab ⊢ ( 𝑡 ∈ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ↔ ( 𝑡 ∈ ( fi ‘ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 ) )
61 60 simprbi ⊢ ( 𝑡 ∈ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∃ 𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 )
62 57 61 syl6 ⊢ ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( 𝑡 ∈ 𝑏 → ∃ 𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 ) )
63 62 ralrimiv ⊢ ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∀ 𝑡 ∈ 𝑏 ∃ 𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 )
64 sseq2 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑡 ) → ( 𝑡 ⊆ 𝑧 ↔ 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) )
65 64 ac6sfi ⊢ ( ( 𝑏 ∈ Fin ∧ ∀ 𝑡 ∈ 𝑏 ∃ 𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 ) → ∃ 𝑓 ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) )
66 65 ex ⊢ ( 𝑏 ∈ Fin → ( ∀ 𝑡 ∈ 𝑏 ∃ 𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 → ∃ 𝑓 ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ) )
67 63 66 syl5 ⊢ ( 𝑏 ∈ Fin → ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∃ 𝑓 ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ) )
68 67 adantl ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) → ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ∃ 𝑓 ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ) )
69 simprll ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → 𝑓 : 𝑏 ⟶ 𝑐 )
70 frn ⊢ ( 𝑓 : 𝑏 ⟶ 𝑐 → ran 𝑓 ⊆ 𝑐 )
71 69 70 syl ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ran 𝑓 ⊆ 𝑐 )
72 simplr ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → 𝑏 ∈ Fin )
73 ffn ⊢ ( 𝑓 : 𝑏 ⟶ 𝑐 → 𝑓 Fn 𝑏 )
74 dffn4 ⊢ ( 𝑓 Fn 𝑏 ↔ 𝑓 : 𝑏 –onto→ ran 𝑓 )
75 73 74 sylib ⊢ ( 𝑓 : 𝑏 ⟶ 𝑐 → 𝑓 : 𝑏 –onto→ ran 𝑓 )
76 75 adantr ⊢ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) → 𝑓 : 𝑏 –onto→ ran 𝑓 )
77 76 ad2antrl ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → 𝑓 : 𝑏 –onto→ ran 𝑓 )
78 fodomfi ⊢ ( ( 𝑏 ∈ Fin ∧ 𝑓 : 𝑏 –onto→ ran 𝑓 ) → ran 𝑓 ≼ 𝑏 )
79 72 77 78 syl2anc ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ran 𝑓 ≼ 𝑏 )
80 domfi ⊢ ( ( 𝑏 ∈ Fin ∧ ran 𝑓 ≼ 𝑏 ) → ran 𝑓 ∈ Fin )
81 72 79 80 syl2anc ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ran 𝑓 ∈ Fin )
82 71 81 jca ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ( ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin ) )
83 elin ⊢ ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ↔ ( ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin ) )
84 vex ⊢ 𝑐 ∈ V
85 84 elpw2 ⊢ ( ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐 )
86 85 anbi1i ⊢ ( ( ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin ) ↔ ( ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin ) )
87 83 86 bitr2i ⊢ ( ( ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin ) ↔ ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) )
88 82 87 sylib ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) )
89 simprr ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → 𝑋 = ∪ 𝑏 )
90 uniiun ⊢ ∪ 𝑏 = ∪ 𝑡 ∈ 𝑏 𝑡
91 simprlr ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) )
92 ss2iun ⊢ ( ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 ( 𝑓 ‘ 𝑡 ) )
93 91 92 syl ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪ 𝑡 ∈ 𝑏 ( 𝑓 ‘ 𝑡 ) )
94 90 93 eqsstrid ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ∪ 𝑏 ⊆ ∪ 𝑡 ∈ 𝑏 ( 𝑓 ‘ 𝑡 ) )
95 fniunfv ⊢ ( 𝑓 Fn 𝑏 → ∪ 𝑡 ∈ 𝑏 ( 𝑓 ‘ 𝑡 ) = ∪ ran 𝑓 )
96 69 73 95 3syl ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ∪ 𝑡 ∈ 𝑏 ( 𝑓 ‘ 𝑡 ) = ∪ ran 𝑓 )
97 94 96 sseqtrd ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ∪ 𝑏 ⊆ ∪ ran 𝑓 )
98 89 97 eqsstrd ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → 𝑋 ⊆ ∪ ran 𝑓 )
99 simpll2 ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → 𝑐 ⊆ 𝐽 )
100 71 99 sstrd ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ran 𝑓 ⊆ 𝐽 )
101 uniss ⊢ ( ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ ∪ 𝐽 )
102 101 1 sseqtrrdi ⊢ ( ran 𝑓 ⊆ 𝐽 → ∪ ran 𝑓 ⊆ 𝑋 )
103 100 102 syl ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ∪ ran 𝑓 ⊆ 𝑋 )
104 98 103 eqssd ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → 𝑋 = ∪ ran 𝑓 )
105 unieq ⊢ ( 𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓 )
106 105 eqeq2d ⊢ ( 𝑑 = ran 𝑓 → ( 𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ ran 𝑓 ) )
107 106 rspcev ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑋 = ∪ ran 𝑓 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 )
108 88 104 107 syl2anc ⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) ∧ ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) ∧ 𝑋 = ∪ 𝑏 ) ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 )
109 108 exp32 ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) → ( ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) → ( 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
110 109 exlimdv ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) → ( ∃ 𝑓 ( 𝑓 : 𝑏 ⟶ 𝑐 ∧ ∀ 𝑡 ∈ 𝑏 𝑡 ⊆ ( 𝑓 ‘ 𝑡 ) ) → ( 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
111 68 110 syld ⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ∧ 𝑏 ∈ Fin ) → ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
112 111 ex ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑏 ∈ Fin → ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
113 112 com23 ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } → ( 𝑏 ∈ Fin → ( 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
114 113 impd ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( ( 𝑏 ⊆ { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∧ 𝑏 ∈ Fin ) → ( 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
115 56 114 syl5bi ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) → ( 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
116 115 rexlimdv ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( ∃ 𝑏 ∈ ( 𝒫 { 𝑦 ∈ ( fi ‘ 𝑥 ) ∣ ∃ 𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 } ∩ Fin ) 𝑋 = ∪ 𝑏 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
117 55 116 syld ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
118 117 3exp ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( 𝑐 ⊆ 𝐽 → ( 𝑋 = ∪ 𝑐 → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
119 118 com34 ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( 𝑐 ⊆ 𝐽 → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
120 119 com23 ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ( 𝑐 ⊆ 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
121 4 120 syl7bi ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
122 121 ralrimdv ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
123 fibas ⊢ ( fi ‘ 𝑥 ) ∈ TopBases
124 tgcl ⊢ ( ( fi ‘ 𝑥 ) ∈ TopBases → ( topGen ‘ ( fi ‘ 𝑥 ) ) ∈ Top )
125 123 124 ax-mp ⊢ ( topGen ‘ ( fi ‘ 𝑥 ) ) ∈ Top
126 eleq1 ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( 𝐽 ∈ Top ↔ ( topGen ‘ ( fi ‘ 𝑥 ) ) ∈ Top ) )
127 125 126 mpbiri ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → 𝐽 ∈ Top )
128 122 127 jctild ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) )
129 1 iscmp ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
130 128 129 syl6ibr ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) → 𝐽 ∈ Comp ) )
131 3 130 syld ⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → 𝐽 ∈ Comp ) )
132 131 imp ⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) → 𝐽 ∈ Comp )
133 132 exlimiv ⊢ ( ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) → 𝐽 ∈ Comp )
134 2 133 impbii ⊢ ( 𝐽 ∈ Comp ↔ ∃ 𝑥 ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )