MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnconn Structured version   Visualization version   GIF version

Theorem cnconn 22925
Description: Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
Hypothesis
Ref Expression
cnconn.2 𝑌 = 𝐾
Assertion
Ref Expression
cnconn ((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn)

Proof of Theorem cnconn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 cntop2 22744 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
213ad2ant3 1135 . 2 ((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top)
3 df-ne 2941 . . . . . . 7 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
4 eqid 2732 . . . . . . . . . . . 12 𝐽 = 𝐽
5 simpl1 1191 . . . . . . . . . . . 12 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐽 ∈ Conn)
6 simpl3 1193 . . . . . . . . . . . . 13 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹 ∈ (𝐽 Cn 𝐾))
7 simprl 769 . . . . . . . . . . . . . 14 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)))
87elin1d 4198 . . . . . . . . . . . . 13 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥𝐾)
9 cnima 22768 . . . . . . . . . . . . 13 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥𝐾) → (𝐹𝑥) ∈ 𝐽)
106, 8, 9syl2anc 584 . . . . . . . . . . . 12 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹𝑥) ∈ 𝐽)
11 elssuni 4941 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐾𝑥 𝐾)
128, 11syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 𝐾)
13 cnconn.2 . . . . . . . . . . . . . . . . . 18 𝑌 = 𝐾
1412, 13sseqtrrdi 4033 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥𝑌)
15 simpl2 1192 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹:𝑋onto𝑌)
16 forn 6808 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑋onto𝑌 → ran 𝐹 = 𝑌)
1715, 16syl 17 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → ran 𝐹 = 𝑌)
1814, 17sseqtrrd 4023 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ran 𝐹)
19 df-rn 5687 . . . . . . . . . . . . . . . 16 ran 𝐹 = dom 𝐹
2018, 19sseqtrdi 4032 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ dom 𝐹)
21 sseqin2 4215 . . . . . . . . . . . . . . 15 (𝑥 ⊆ dom 𝐹 ↔ (dom 𝐹𝑥) = 𝑥)
2220, 21sylib 217 . . . . . . . . . . . . . 14 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom 𝐹𝑥) = 𝑥)
23 simprr 771 . . . . . . . . . . . . . 14 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅)
2422, 23eqnetrd 3008 . . . . . . . . . . . . 13 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom 𝐹𝑥) ≠ ∅)
25 imadisj 6079 . . . . . . . . . . . . . 14 ((𝐹𝑥) = ∅ ↔ (dom 𝐹𝑥) = ∅)
2625necon3bii 2993 . . . . . . . . . . . . 13 ((𝐹𝑥) ≠ ∅ ↔ (dom 𝐹𝑥) ≠ ∅)
2724, 26sylibr 233 . . . . . . . . . . . 12 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹𝑥) ≠ ∅)
287elin2d 4199 . . . . . . . . . . . . 13 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (Clsd‘𝐾))
29 cnclima 22771 . . . . . . . . . . . . 13 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ (Clsd‘𝐾)) → (𝐹𝑥) ∈ (Clsd‘𝐽))
306, 28, 29syl2anc 584 . . . . . . . . . . . 12 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹𝑥) ∈ (Clsd‘𝐽))
314, 5, 10, 27, 30connclo 22918 . . . . . . . . . . 11 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹𝑥) = 𝐽)
324, 13cnf 22749 . . . . . . . . . . . 12 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽𝑌)
33 fdm 6726 . . . . . . . . . . . 12 (𝐹: 𝐽𝑌 → dom 𝐹 = 𝐽)
346, 32, 333syl 18 . . . . . . . . . . 11 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = 𝐽)
35 fof 6805 . . . . . . . . . . . 12 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
36 fdm 6726 . . . . . . . . . . . 12 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
3715, 35, 363syl 18 . . . . . . . . . . 11 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = 𝑋)
3831, 34, 373eqtr2d 2778 . . . . . . . . . 10 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹𝑥) = 𝑋)
3938imaeq2d 6059 . . . . . . . . 9 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (𝐹𝑥)) = (𝐹𝑋))
40 foimacnv 6850 . . . . . . . . . 10 ((𝐹:𝑋onto𝑌𝑥𝑌) → (𝐹 “ (𝐹𝑥)) = 𝑥)
4115, 14, 40syl2anc 584 . . . . . . . . 9 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (𝐹𝑥)) = 𝑥)
42 foima 6810 . . . . . . . . . 10 (𝐹:𝑋onto𝑌 → (𝐹𝑋) = 𝑌)
4315, 42syl 17 . . . . . . . . 9 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹𝑋) = 𝑌)
4439, 41, 433eqtr3d 2780 . . . . . . . 8 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 = 𝑌)
4544expr 457 . . . . . . 7 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 ≠ ∅ → 𝑥 = 𝑌))
463, 45biimtrrid 242 . . . . . 6 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (¬ 𝑥 = ∅ → 𝑥 = 𝑌))
4746orrd 861 . . . . 5 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 = ∅ ∨ 𝑥 = 𝑌))
48 vex 3478 . . . . . 6 𝑥 ∈ V
4948elpr 4651 . . . . 5 (𝑥 ∈ {∅, 𝑌} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝑌))
5047, 49sylibr 233 . . . 4 (((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → 𝑥 ∈ {∅, 𝑌})
5150ex 413 . . 3 ((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) → 𝑥 ∈ {∅, 𝑌}))
5251ssrdv 3988 . 2 ((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌})
5313isconn2 22917 . 2 (𝐾 ∈ Conn ↔ (𝐾 ∈ Top ∧ (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌}))
542, 52, 53sylanbrc 583 1 ((𝐽 ∈ Conn ∧ 𝐹:𝑋onto𝑌𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2940  cin 3947  wss 3948  c0 4322  {cpr 4630   cuni 4908  ccnv 5675  dom cdm 5676  ran crn 5677  cima 5679  wf 6539  ontowfo 6541  cfv 6543  (class class class)co 7408  Topctop 22394  Clsdccld 22519   Cn ccn 22727  Conncconn 22914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fo 6549  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-map 8821  df-top 22395  df-topon 22412  df-cld 22522  df-cn 22730  df-conn 22915
This theorem is referenced by:  connima  22928  conncn  22929  qtopconn  23212  connhmph  23292  ivthALT  35215
  Copyright terms: Public domain W3C validator