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

Theorem cnrest2 22446
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 22400 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
21a1i 11 . . 3 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top))
3 eqid 2739 . . . . . . . 8 𝐽 = 𝐽
4 eqid 2739 . . . . . . . 8 𝐾 = 𝐾
53, 4cnf 22406 . . . . . . 7 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
65ffnd 6610 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn 𝐽)
76a1i 11 . . . . 5 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn 𝐽))
8 simp2 1136 . . . . 5 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → ran 𝐹𝐵)
97, 8jctird 527 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹 Fn 𝐽 ∧ ran 𝐹𝐵)))
10 df-f 6441 . . . 4 (𝐹: 𝐽𝐵 ↔ (𝐹 Fn 𝐽 ∧ ran 𝐹𝐵))
119, 10syl6ibr 251 . . 3 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽𝐵))
122, 11jcad 513 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)))
13 cntop1 22400 . . . . 5 (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) → 𝐽 ∈ Top)
1413adantl 482 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐽 ∈ Top)
15 toptopon2 22076 . . . . . 6 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
1614, 15sylib 217 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐽 ∈ (TopOn‘ 𝐽))
17 resttopon 22321 . . . . . . 7 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵𝑌) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
18173adant2 1130 . . . . . 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 22409 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (𝐾t 𝐵) ∈ (TopOn‘𝐵) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹: 𝐽𝐵)
2216, 19, 20, 21syl3anc 1370 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹: 𝐽𝐵)
2314, 22jca 512 . . 3 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵))
2423ex 413 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)))
25 vex 3437 . . . . . . . . 9 𝑥 ∈ V
2625inex1 5242 . . . . . . . 8 (𝑥𝐵) ∈ V
2726a1i 11 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝑥𝐵) ∈ V)
28 simpl1 1190 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐾 ∈ (TopOn‘𝑌))
29 toponmax 22084 . . . . . . . . . 10 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
3028, 29syl 17 . . . . . . . . 9 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝑌𝐾)
31 simpl3 1192 . . . . . . . . 9 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐵𝑌)
3230, 31ssexd 5249 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐵 ∈ V)
33 elrest 17147 . . . . . . . 8 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ V) → (𝑦 ∈ (𝐾t 𝐵) ↔ ∃𝑥𝐾 𝑦 = (𝑥𝐵)))
3428, 32, 33syl2anc 584 . . . . . . 7 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝑦 ∈ (𝐾t 𝐵) ↔ ∃𝑥𝐾 𝑦 = (𝑥𝐵)))
35 imaeq2 5968 . . . . . . . . 9 (𝑦 = (𝑥𝐵) → (𝐹𝑦) = (𝐹 “ (𝑥𝐵)))
3635eleq1d 2824 . . . . . . . 8 (𝑦 = (𝑥𝐵) → ((𝐹𝑦) ∈ 𝐽 ↔ (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
3736adantl 482 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑦 = (𝑥𝐵)) → ((𝐹𝑦) ∈ 𝐽 ↔ (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
3827, 34, 37ralxfr2d 5334 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽 ↔ ∀𝑥𝐾 (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
39 simplrr 775 . . . . . . . . . 10 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → 𝐹: 𝐽𝐵)
40 ffun 6612 . . . . . . . . . 10 (𝐹: 𝐽𝐵 → Fun 𝐹)
41 inpreima 6950 . . . . . . . . . 10 (Fun 𝐹 → (𝐹 “ (𝑥𝐵)) = ((𝐹𝑥) ∩ (𝐹𝐵)))
4239, 40, 413syl 18 . . . . . . . . 9 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ (𝑥𝐵)) = ((𝐹𝑥) ∩ (𝐹𝐵)))
43 cnvimass 5992 . . . . . . . . . . . 12 (𝐹𝑥) ⊆ dom 𝐹
44 cnvimarndm 5993 . . . . . . . . . . . 12 (𝐹 “ ran 𝐹) = dom 𝐹
4543, 44sseqtrri 3959 . . . . . . . . . . 11 (𝐹𝑥) ⊆ (𝐹 “ ran 𝐹)
46 simpll2 1212 . . . . . . . . . . . 12 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ran 𝐹𝐵)
47 imass2 6013 . . . . . . . . . . . 12 (ran 𝐹𝐵 → (𝐹 “ ran 𝐹) ⊆ (𝐹𝐵))
4846, 47syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ ran 𝐹) ⊆ (𝐹𝐵))
4945, 48sstrid 3933 . . . . . . . . . 10 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹𝑥) ⊆ (𝐹𝐵))
50 df-ss 3905 . . . . . . . . . 10 ((𝐹𝑥) ⊆ (𝐹𝐵) ↔ ((𝐹𝑥) ∩ (𝐹𝐵)) = (𝐹𝑥))
5149, 50sylib 217 . . . . . . . . 9 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ((𝐹𝑥) ∩ (𝐹𝐵)) = (𝐹𝑥))
5242, 51eqtrd 2779 . . . . . . . 8 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ (𝑥𝐵)) = (𝐹𝑥))
5352eleq1d 2824 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ((𝐹 “ (𝑥𝐵)) ∈ 𝐽 ↔ (𝐹𝑥) ∈ 𝐽))
5453ralbidva 3112 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑥𝐾 (𝐹 “ (𝑥𝐵)) ∈ 𝐽 ↔ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽))
55 simprr 770 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐹: 𝐽𝐵)
5655, 31fssd 6627 . . . . . . 7 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐹: 𝐽𝑌)
5756biantrurd 533 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽 ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
5838, 54, 573bitrrd 306 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → ((𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽) ↔ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽))
5955biantrurd 533 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽 ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6058, 59bitrd 278 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → ((𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
61 simprl 768 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐽 ∈ Top)
6261, 15sylib 217 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐽 ∈ (TopOn‘ 𝐽))
63 iscn 22395 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
6462, 28, 63syl2anc 584 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
6518adantr 481 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
66 iscn 22395 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (𝐾t 𝐵) ∈ (TopOn‘𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6762, 65, 66syl2anc 584 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6860, 64, 673bitr4d 311 . . 3 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))))
6968ex 413 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → ((𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)))))
7012, 24, 69pm5.21ndd 381 1 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2107  wral 3065  wrex 3066  Vcvv 3433  cin 3887  wss 3888   cuni 4840  ccnv 5589  dom cdm 5590  ran crn 5591  cima 5593  Fun wfun 6431   Fn wfn 6432  wf 6433  cfv 6437  (class class class)co 7284  t crest 17140  Topctop 22051  TopOnctopon 22068   Cn ccn 22384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-map 8626  df-en 8743  df-fin 8746  df-fi 9179  df-rest 17142  df-topgen 17163  df-top 22052  df-topon 22069  df-bases 22105  df-cn 22387
This theorem is referenced by:  cnrest2r  22447  rncmp  22556  connima  22585  conncn  22586  kgencn2  22717  kgencn3  22718  qtoprest  22877  hmeores  22931  efmndtmd  23261  submtmd  23264  subgtgp  23265  symgtgp  23266  metdcn2  24011  metdscn2  24029  cnmptre  24099  iimulcn  24110  icchmeo  24113  evth  24131  evth2  24132  lebnumlem2  24134  reparphti  24169  efrlim  26128  rmulccn  31887  raddcn  31888  xrge0mulc1cn  31900  cvxpconn  33213  cvxsconn  33214  cvmliftmolem1  33252  cvmliftlem8  33263  cvmlift2lem9  33282  cvmlift3lem6  33295  ivthALT  34533  knoppcnlem10  34691  broucube  35820  areacirclem2  35875  cnres2  35930  cnresima  35931  refsumcn  42580  icccncfext  43435
  Copyright terms: Public domain W3C validator