Metamath Proof Explorer

Theorem cnconn

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

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

Proof

Step Hyp Ref Expression
1 cnconn.2 ⊢ 𝑌 = ∪ 𝐾
2 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
3 2 3ad2ant3 ⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Top )
4 df-ne ⊢ ( 𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅ )
5 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
6 simpl1 ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝐽 ∈ Conn )
7 simpl3 ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
8 simprl ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) )
9 8 elin1d ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ 𝐾 )
10 cnima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
11 7 9 10 syl2anc ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
12 elssuni ⊢ ( 𝑥 ∈ 𝐾 → 𝑥 ⊆ ∪ 𝐾 )
13 9 12 syl ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ⊆ ∪ 𝐾 )
14 13 1 sseqtrrdi ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ⊆ 𝑌 )
15 simpl2 ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
16 forn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
17 15 16 syl ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ran 𝐹 = 𝑌 )
18 14 17 sseqtrrd ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ⊆ ran 𝐹 )
19 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
20 18 19 sseqtrdi ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ⊆ dom ◡ 𝐹 )
21 sseqin2 ⊢ ( 𝑥 ⊆ dom ◡ 𝐹 ↔ ( dom ◡ 𝐹 ∩ 𝑥 ) = 𝑥 )
22 20 21 sylib ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( dom ◡ 𝐹 ∩ 𝑥 ) = 𝑥 )
23 simprr ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ≠ ∅ )
24 22 23 eqnetrd ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( dom ◡ 𝐹 ∩ 𝑥 ) ≠ ∅ )
25 imadisj ⊢ ( ( ◡ 𝐹 “ 𝑥 ) = ∅ ↔ ( dom ◡ 𝐹 ∩ 𝑥 ) = ∅ )
26 25 necon3bii ⊢ ( ( ◡ 𝐹 “ 𝑥 ) ≠ ∅ ↔ ( dom ◡ 𝐹 ∩ 𝑥 ) ≠ ∅ )
27 24 26 sylibr ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( ◡ 𝐹 “ 𝑥 ) ≠ ∅ )
28 8 elin2d ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ ( Clsd ‘ 𝐾 ) )
29 cnclima ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
30 7 28 29 syl2anc ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
31 5 6 11 27 30 connclo ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( ◡ 𝐹 “ 𝑥 ) = ∪ 𝐽 )
32 5 1 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 )
33 fdm ⊢ ( 𝐹 : ∪ 𝐽 ⟶ 𝑌 → dom 𝐹 = ∪ 𝐽 )
34 7 32 33 3syl ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → dom 𝐹 = ∪ 𝐽 )
35 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
36 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
37 15 35 36 3syl ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → dom 𝐹 = 𝑋 )
38 31 34 37 3eqtr2d ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( ◡ 𝐹 “ 𝑥 ) = 𝑋 )
39 38 imaeq2d ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝐹 “ 𝑋 ) )
40 foimacnv ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑥 ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = 𝑥 )
41 15 14 40 syl2anc ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) = 𝑥 )
42 foima ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( 𝐹 “ 𝑋 ) = 𝑌 )
43 15 42 syl ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → ( 𝐹 “ 𝑋 ) = 𝑌 )
44 39 41 43 3eqtr3d ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ∧ 𝑥 ≠ ∅ ) ) → 𝑥 = 𝑌 )
45 44 expr ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ) → ( 𝑥 ≠ ∅ → 𝑥 = 𝑌 ) )
46 4 45 biimtrrid ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ) → ( ¬ 𝑥 = ∅ → 𝑥 = 𝑌 ) )
47 46 orrd ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ) → ( 𝑥 = ∅ ∨ 𝑥 = 𝑌 ) )
48 vex ⊢ 𝑥 ∈ V
49 48 elpr ⊢ ( 𝑥 ∈ { ∅ , 𝑌 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = 𝑌 ) )
50 47 49 sylibr ⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ) → 𝑥 ∈ { ∅ , 𝑌 } )
51 50 ex ⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑥 ∈ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) → 𝑥 ∈ { ∅ , 𝑌 } ) )
52 51 ssrdv ⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ⊆ { ∅ , 𝑌 } )
53 1 isconn2 ⊢ ( 𝐾 ∈ Conn ↔ ( 𝐾 ∈ Top ∧ ( 𝐾 ∩ ( Clsd ‘ 𝐾 ) ) ⊆ { ∅ , 𝑌 } ) )
54 3 52 53 sylanbrc ⊢ ( ( 𝐽 ∈ Conn ∧ 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Conn )