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

Theorem cnrest2 22719
Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnrest2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))))

Proof of Theorem cnrest2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cntop1 22673 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
21a1i 11 . . 3 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top))
3 eqid 2731 . . . . . . . 8 𝐽 = 𝐽
4 eqid 2731 . . . . . . . 8 𝐾 = 𝐾
53, 4cnf 22679 . . . . . . 7 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
65ffnd 6705 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn 𝐽)
76a1i 11 . . . . 5 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn 𝐽))
8 simp2 1137 . . . . 5 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → ran 𝐹𝐵)
97, 8jctird 527 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹 Fn 𝐽 ∧ ran 𝐹𝐵)))
10 df-f 6536 . . . 4 (𝐹: 𝐽𝐵 ↔ (𝐹 Fn 𝐽 ∧ ran 𝐹𝐵))
119, 10syl6ibr 251 . . 3 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽𝐵))
122, 11jcad 513 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)))
13 cntop1 22673 . . . . 5 (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) → 𝐽 ∈ Top)
1413adantl 482 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐽 ∈ Top)
15 toptopon2 22349 . . . . . 6 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
1614, 15sylib 217 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐽 ∈ (TopOn‘ 𝐽))
17 resttopon 22594 . . . . . . 7 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵𝑌) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
18173adant2 1131 . . . . . 6 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
1918adantr 481 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
20 simpr 485 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)))
21 cnf2 22682 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (𝐾t 𝐵) ∈ (TopOn‘𝐵) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹: 𝐽𝐵)
2216, 19, 20, 21syl3anc 1371 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹: 𝐽𝐵)
2314, 22jca 512 . . 3 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵))
2423ex 413 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)))
25 vex 3477 . . . . . . . . 9 𝑥 ∈ V
2625inex1 5310 . . . . . . . 8 (𝑥𝐵) ∈ V
2726a1i 11 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝑥𝐵) ∈ V)
28 simpl1 1191 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐾 ∈ (TopOn‘𝑌))
29 toponmax 22357 . . . . . . . . . 10 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
3028, 29syl 17 . . . . . . . . 9 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝑌𝐾)
31 simpl3 1193 . . . . . . . . 9 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐵𝑌)
3230, 31ssexd 5317 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐵 ∈ V)
33 elrest 17355 . . . . . . . 8 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ V) → (𝑦 ∈ (𝐾t 𝐵) ↔ ∃𝑥𝐾 𝑦 = (𝑥𝐵)))
3428, 32, 33syl2anc 584 . . . . . . 7 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝑦 ∈ (𝐾t 𝐵) ↔ ∃𝑥𝐾 𝑦 = (𝑥𝐵)))
35 imaeq2 6045 . . . . . . . . 9 (𝑦 = (𝑥𝐵) → (𝐹𝑦) = (𝐹 “ (𝑥𝐵)))
3635eleq1d 2817 . . . . . . . 8 (𝑦 = (𝑥𝐵) → ((𝐹𝑦) ∈ 𝐽 ↔ (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
3736adantl 482 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑦 = (𝑥𝐵)) → ((𝐹𝑦) ∈ 𝐽 ↔ (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
3827, 34, 37ralxfr2d 5401 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽 ↔ ∀𝑥𝐾 (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
39 simplrr 776 . . . . . . . . . 10 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → 𝐹: 𝐽𝐵)
40 ffun 6707 . . . . . . . . . 10 (𝐹: 𝐽𝐵 → Fun 𝐹)
41 inpreima 7050 . . . . . . . . . 10 (Fun 𝐹 → (𝐹 “ (𝑥𝐵)) = ((𝐹𝑥) ∩ (𝐹𝐵)))
4239, 40, 413syl 18 . . . . . . . . 9 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ (𝑥𝐵)) = ((𝐹𝑥) ∩ (𝐹𝐵)))
43 cnvimass 6069 . . . . . . . . . . . 12 (𝐹𝑥) ⊆ dom 𝐹
44 cnvimarndm 6070 . . . . . . . . . . . 12 (𝐹 “ ran 𝐹) = dom 𝐹
4543, 44sseqtrri 4015 . . . . . . . . . . 11 (𝐹𝑥) ⊆ (𝐹 “ ran 𝐹)
46 simpll2 1213 . . . . . . . . . . . 12 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ran 𝐹𝐵)
47 imass2 6090 . . . . . . . . . . . 12 (ran 𝐹𝐵 → (𝐹 “ ran 𝐹) ⊆ (𝐹𝐵))
4846, 47syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ ran 𝐹) ⊆ (𝐹𝐵))
4945, 48sstrid 3989 . . . . . . . . . 10 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹𝑥) ⊆ (𝐹𝐵))
50 df-ss 3961 . . . . . . . . . 10 ((𝐹𝑥) ⊆ (𝐹𝐵) ↔ ((𝐹𝑥) ∩ (𝐹𝐵)) = (𝐹𝑥))
5149, 50sylib 217 . . . . . . . . 9 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ((𝐹𝑥) ∩ (𝐹𝐵)) = (𝐹𝑥))
5242, 51eqtrd 2771 . . . . . . . 8 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ (𝑥𝐵)) = (𝐹𝑥))
5352eleq1d 2817 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ((𝐹 “ (𝑥𝐵)) ∈ 𝐽 ↔ (𝐹𝑥) ∈ 𝐽))
5453ralbidva 3174 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑥𝐾 (𝐹 “ (𝑥𝐵)) ∈ 𝐽 ↔ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽))
55 simprr 771 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐹: 𝐽𝐵)
5655, 31fssd 6722 . . . . . . 7 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐹: 𝐽𝑌)
5756biantrurd 533 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽 ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
5838, 54, 573bitrrd 305 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → ((𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽) ↔ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽))
5955biantrurd 533 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽 ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6058, 59bitrd 278 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → ((𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
61 simprl 769 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐽 ∈ Top)
6261, 15sylib 217 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐽 ∈ (TopOn‘ 𝐽))
63 iscn 22668 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
6462, 28, 63syl2anc 584 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
6518adantr 481 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
66 iscn 22668 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (𝐾t 𝐵) ∈ (TopOn‘𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6762, 65, 66syl2anc 584 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6860, 64, 673bitr4d 310 . . 3 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))))
6968ex 413 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → ((𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)))))
7012, 24, 69pm5.21ndd 380 1 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3060  wrex 3069  Vcvv 3473  cin 3943  wss 3944   cuni 4901  ccnv 5668  dom cdm 5669  ran crn 5670  cima 5672  Fun wfun 6526   Fn wfn 6527  wf 6528  cfv 6532  (class class class)co 7393  t crest 17348  Topctop 22324  TopOnctopon 22341   Cn ccn 22657
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 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-1st 7957  df-2nd 7958  df-map 8805  df-en 8923  df-fin 8926  df-fi 9388  df-rest 17350  df-topgen 17371  df-top 22325  df-topon 22342  df-bases 22378  df-cn 22660
This theorem is referenced by:  cnrest2r  22720  rncmp  22829  connima  22858  conncn  22859  kgencn2  22990  kgencn3  22991  qtoprest  23150  hmeores  23204  efmndtmd  23534  submtmd  23537  subgtgp  23538  symgtgp  23539  metdcn2  24284  metdscn2  24302  cnmptre  24372  iimulcn  24383  icchmeo  24386  evth  24404  evth2  24405  lebnumlem2  24407  reparphti  24442  efrlim  26401  rmulccn  32737  raddcn  32738  xrge0mulc1cn  32750  cvxpconn  34062  cvxsconn  34063  cvmliftmolem1  34101  cvmliftlem8  34112  cvmlift2lem9  34131  cvmlift3lem6  34144  ivthALT  35022  knoppcnlem10  35180  broucube  36324  areacirclem2  36379  cnres2  36434  cnresima  36435  refsumcn  43483  icccncfext  44374
  Copyright terms: Public domain W3C validator