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 ⊢ X = ⋃ J
connima.f ⊢ φ → F ∈ J Cn K
connima.a ⊢ φ → A ⊆ X
connima.c ⊢ φ → J ↾ 𝑡 A ∈ Conn
Assertion connima ⊢ φ → K ↾ 𝑡 F A ∈ Conn

Proof

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