Metamath Proof Explorer

Theorem connima

Description: The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses connima.x ⊢ 𝑋 = ∪ 𝐽
connima.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
connima.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
connima.c ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ∈ Conn )
Assertion connima ( 𝜑 → ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 connima.x ⊢ 𝑋 = ∪ 𝐽
2 connima.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 connima.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4 connima.c ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ∈ Conn )
5 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
6 1 5 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
7 2 6 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
8 7 ffund ⊢ ( 𝜑 → Fun 𝐹 )
9 7 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
10 3 9 sseqtrrd ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
11 fores ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )
12 8 10 11 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )
13 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
14 2 13 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
15 imassrn ⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
16 7 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ∪ 𝐾 )
17 15 16 sstrid ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ ∪ 𝐾 )
18 5 restuni ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐹 “ 𝐴 ) ⊆ ∪ 𝐾 ) → ( 𝐹 “ 𝐴 ) = ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) )
19 14 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) = ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) )
20 foeq3 ⊢ ( ( 𝐹 “ 𝐴 ) = ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ) )
21 19 20 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ) )
22 12 21 mpbid ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) )
23 1 cnrest ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
24 2 3 23 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
25 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
26 14 25 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
27 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
28 eqimss2 ⊢ ( ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 ) → ran ( 𝐹 ↾ 𝐴 ) ⊆ ( 𝐹 “ 𝐴 ) )
29 27 28 mp1i ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝐴 ) ⊆ ( 𝐹 “ 𝐴 ) )
30 cnrest2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ran ( 𝐹 ↾ 𝐴 ) ⊆ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ ∪ 𝐾 ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ) ) )
31 26 29 17 30 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ) ) )
32 24 31 mpbid ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ) )
33 eqid ⊢ ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) )
34 33 cnconn ⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ Conn ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ∪ ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ∧ ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ) ) → ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ∈ Conn )
35 4 22 32 34 syl3anc ⊢ ( 𝜑 → ( 𝐾 ↾t ( 𝐹 “ 𝐴 ) ) ∈ Conn )