Metamath Proof Explorer

Theorem cncmp

Description: Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis cncmp.2 ⊢ 𝑌 = ∪ 𝐾
Assertion cncmp ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Comp )

Proof

Step Hyp Ref Expression
1 cncmp.2 ⊢ 𝑌 = ∪ 𝐾
2 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
3 2 3ad2ant3 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Top )
4 elpwi ⊢ ( 𝑢 ∈ 𝒫 𝐾 → 𝑢 ⊆ 𝐾 )
5 simpl1 ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → 𝐽 ∈ Comp )
6 simpl3 ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7 simprl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → 𝑢 ⊆ 𝐾 )
8 7 sselda ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑦 ∈ 𝑢 ) → 𝑦 ∈ 𝐾 )
9 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑦 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
10 6 8 9 syl2an2r ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑦 ∈ 𝑢 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
11 10 fmpttd ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) : 𝑢 ⟶ 𝐽 )
12 11 frnd ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ 𝐽 )
13 simprr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → 𝑌 = ∪ 𝑢 )
14 13 imaeq2d ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ( ◡ 𝐹 “ 𝑌 ) = ( ◡ 𝐹 “ ∪ 𝑢 ) )
15 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
16 15 1 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
17 6 16 syl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
18 fimacnv ⊢ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 → ( ◡ 𝐹 “ 𝑌 ) = ∪ 𝐽 )
19 17 18 syl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ( ◡ 𝐹 “ 𝑌 ) = ∪ 𝐽 )
20 10 ralrimiva ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ∀ 𝑦 ∈ 𝑢 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
21 dfiun2g ⊢ ( ∀ 𝑦 ∈ 𝑢 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∪ 𝑦 ∈ 𝑢 ( ◡ 𝐹 “ 𝑦 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑢 𝑥 = ( ◡ 𝐹 “ 𝑦 ) } )
22 20 21 syl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ∪ 𝑦 ∈ 𝑢 ( ◡ 𝐹 “ 𝑦 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑢 𝑥 = ( ◡ 𝐹 “ 𝑦 ) } )
23 imauni ⊢ ( ◡ 𝐹 “ ∪ 𝑢 ) = ∪ 𝑦 ∈ 𝑢 ( ◡ 𝐹 “ 𝑦 )
24 eqid ⊢ ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) = ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) )
25 24 rnmpt ⊢ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑢 𝑥 = ( ◡ 𝐹 “ 𝑦 ) }
26 25 unieqi ⊢ ∪ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑢 𝑥 = ( ◡ 𝐹 “ 𝑦 ) }
27 22 23 26 3eqtr4g ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ( ◡ 𝐹 “ ∪ 𝑢 ) = ∪ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) )
28 14 19 27 3eqtr3d ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ∪ 𝐽 = ∪ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) )
29 15 cmpcov ⊢ ( ( 𝐽 ∈ Comp ∧ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ) → ∃ 𝑠 ∈ ( 𝒫 ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∩ Fin ) ∪ 𝐽 = ∪ 𝑠 )
30 5 12 28 29 syl3anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ∃ 𝑠 ∈ ( 𝒫 ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∩ Fin ) ∪ 𝐽 = ∪ 𝑠 )
31 elfpw ⊢ ( 𝑠 ∈ ( 𝒫 ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∩ Fin ) ↔ ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) )
32 simprll ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) )
33 32 sselda ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) ∧ 𝑐 ∈ 𝑠 ) → 𝑐 ∈ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) )
34 simpll2 ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑦 ∈ 𝑢 ) → 𝐹 : 𝑋 –onto→ 𝑌 )
35 elssuni ⊢ ( 𝑦 ∈ 𝐾 → 𝑦 ⊆ ∪ 𝐾 )
36 35 1 sseqtrrdi ⊢ ( 𝑦 ∈ 𝐾 → 𝑦 ⊆ 𝑌 )
37 8 36 syl ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑦 ∈ 𝑢 ) → 𝑦 ⊆ 𝑌 )
38 foimacnv ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
39 34 37 38 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑦 ∈ 𝑢 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 )
40 simpr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑦 ∈ 𝑢 ) → 𝑦 ∈ 𝑢 )
41 39 40 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑦 ∈ 𝑢 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝑢 )
42 41 ralrimiva ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ∀ 𝑦 ∈ 𝑢 ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝑢 )
43 imaeq2 ⊢ ( 𝑐 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 “ 𝑐 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) )
44 43 eleq1d ⊢ ( 𝑐 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝐹 “ 𝑐 ) ∈ 𝑢 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝑢 ) )
45 24 44 ralrnmptw ⊢ ( ∀ 𝑦 ∈ 𝑢 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ∀ 𝑐 ∈ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ( 𝐹 “ 𝑐 ) ∈ 𝑢 ↔ ∀ 𝑦 ∈ 𝑢 ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝑢 ) )
46 20 45 syl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ( ∀ 𝑐 ∈ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ( 𝐹 “ 𝑐 ) ∈ 𝑢 ↔ ∀ 𝑦 ∈ 𝑢 ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝑢 ) )
47 42 46 mpbird ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ∀ 𝑐 ∈ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ( 𝐹 “ 𝑐 ) ∈ 𝑢 )
48 47 adantr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ∀ 𝑐 ∈ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ( 𝐹 “ 𝑐 ) ∈ 𝑢 )
49 48 r19.21bi ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) ∧ 𝑐 ∈ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ) → ( 𝐹 “ 𝑐 ) ∈ 𝑢 )
50 33 49 syldan ⊢ ( ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) ∧ 𝑐 ∈ 𝑠 ) → ( 𝐹 “ 𝑐 ) ∈ 𝑢 )
51 50 fmpttd ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) : 𝑠 ⟶ 𝑢 )
52 51 frnd ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ⊆ 𝑢 )
53 simprlr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → 𝑠 ∈ Fin )
54 eqid ⊢ ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) = ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) )
55 54 rnmpt ⊢ ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) = { 𝑑 ∣ ∃ 𝑐 ∈ 𝑠 𝑑 = ( 𝐹 “ 𝑐 ) }
56 abrexfi ⊢ ( 𝑠 ∈ Fin → { 𝑑 ∣ ∃ 𝑐 ∈ 𝑠 𝑑 = ( 𝐹 “ 𝑐 ) } ∈ Fin )
57 55 56 eqeltrid ⊢ ( 𝑠 ∈ Fin → ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ∈ Fin )
58 53 57 syl ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ∈ Fin )
59 elfpw ⊢ ( ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ⊆ 𝑢 ∧ ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ∈ Fin ) )
60 52 58 59 sylanbrc ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ∈ ( 𝒫 𝑢 ∩ Fin ) )
61 17 adantr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
62 61 fdmd ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → dom 𝐹 = ∪ 𝐽 )
63 simpll2 ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
64 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
65 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
66 63 64 65 3syl ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → dom 𝐹 = 𝑋 )
67 simprr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ∪ 𝐽 = ∪ 𝑠 )
68 62 66 67 3eqtr3d ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → 𝑋 = ∪ 𝑠 )
69 68 imaeq2d ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ( 𝐹 “ 𝑋 ) = ( 𝐹 “ ∪ 𝑠 ) )
70 foima ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( 𝐹 “ 𝑋 ) = 𝑌 )
71 63 70 syl ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ( 𝐹 “ 𝑋 ) = 𝑌 )
72 50 ralrimiva ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ∀ 𝑐 ∈ 𝑠 ( 𝐹 “ 𝑐 ) ∈ 𝑢 )
73 dfiun2g ⊢ ( ∀ 𝑐 ∈ 𝑠 ( 𝐹 “ 𝑐 ) ∈ 𝑢 → ∪ 𝑐 ∈ 𝑠 ( 𝐹 “ 𝑐 ) = ∪ { 𝑑 ∣ ∃ 𝑐 ∈ 𝑠 𝑑 = ( 𝐹 “ 𝑐 ) } )
74 72 73 syl ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ∪ 𝑐 ∈ 𝑠 ( 𝐹 “ 𝑐 ) = ∪ { 𝑑 ∣ ∃ 𝑐 ∈ 𝑠 𝑑 = ( 𝐹 “ 𝑐 ) } )
75 imauni ⊢ ( 𝐹 “ ∪ 𝑠 ) = ∪ 𝑐 ∈ 𝑠 ( 𝐹 “ 𝑐 )
76 55 unieqi ⊢ ∪ ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) = ∪ { 𝑑 ∣ ∃ 𝑐 ∈ 𝑠 𝑑 = ( 𝐹 “ 𝑐 ) }
77 74 75 76 3eqtr4g ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ( 𝐹 “ ∪ 𝑠 ) = ∪ ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) )
78 69 71 77 3eqtr3d ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → 𝑌 = ∪ ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) )
79 unieq ⊢ ( 𝑣 = ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) → ∪ 𝑣 = ∪ ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) )
80 79 rspceeqv ⊢ ( ( ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑌 = ∪ ran ( 𝑐 ∈ 𝑠 ↦ ( 𝐹 “ 𝑐 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 )
81 60 78 80 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ∧ ∪ 𝐽 = ∪ 𝑠 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 )
82 81 expr ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ ( 𝑠 ⊆ ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∧ 𝑠 ∈ Fin ) ) → ( ∪ 𝐽 = ∪ 𝑠 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 ) )
83 31 82 sylan2b ⊢ ( ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) ∧ 𝑠 ∈ ( 𝒫 ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∩ Fin ) ) → ( ∪ 𝐽 = ∪ 𝑠 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 ) )
84 83 rexlimdva ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ( ∃ 𝑠 ∈ ( 𝒫 ran ( 𝑦 ∈ 𝑢 ↦ ( ◡ 𝐹 “ 𝑦 ) ) ∩ Fin ) ∪ 𝐽 = ∪ 𝑠 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 ) )
85 30 84 mpd ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑢 ⊆ 𝐾 ∧ 𝑌 = ∪ 𝑢 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 )
86 85 expr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑢 ⊆ 𝐾 ) → ( 𝑌 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 ) )
87 4 86 sylan2 ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑢 ∈ 𝒫 𝐾 ) → ( 𝑌 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 ) )
88 87 ralrimiva ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑢 ∈ 𝒫 𝐾 ( 𝑌 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 ) )
89 1 iscmp ⊢ ( 𝐾 ∈ Comp ↔ ( 𝐾 ∈ Top ∧ ∀ 𝑢 ∈ 𝒫 𝐾 ( 𝑌 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑌 = ∪ 𝑣 ) ) )
90 3 88 89 sylanbrc ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Comp )