Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnrest2 GIF version

Theorem cnrest2 12442
 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 12407 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
21a1i 9 . . 3 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top))
3 eqid 2140 . . . . . . . 8 𝐽 = 𝐽
4 eqid 2140 . . . . . . . 8 𝐾 = 𝐾
53, 4cnf 12410 . . . . . . 7 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽 𝐾)
65ffnd 5280 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn 𝐽)
76a1i 9 . . . . 5 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn 𝐽))
8 simp2 983 . . . . 5 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → ran 𝐹𝐵)
97, 8jctird 315 . . . 4 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹 Fn 𝐽 ∧ ran 𝐹𝐵)))
10 df-f 5134 . . . 4 (𝐹: 𝐽𝐵 ↔ (𝐹 Fn 𝐽 ∧ ran 𝐹𝐵))
119, 10syl6ibr 161 . . 3 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽𝐵))
122, 11jcad 305 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)))
13 cntop1 12407 . . . . 5 (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) → 𝐽 ∈ Top)
1413adantl 275 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐽 ∈ Top)
153toptopon 12222 . . . . . 6 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
1614, 15sylib 121 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐽 ∈ (TopOn‘ 𝐽))
17 resttopon 12377 . . . . . . 7 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵𝑌) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
18173adant2 1001 . . . . . 6 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
1918adantr 274 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
20 simpr 109 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)))
21 cnf2 12411 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (𝐾t 𝐵) ∈ (TopOn‘𝐵) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹: 𝐽𝐵)
2216, 19, 20, 21syl3anc 1217 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → 𝐹: 𝐽𝐵)
2314, 22jca 304 . . 3 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵))
2423ex 114 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) → (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)))
25 vex 2692 . . . . . . . . 9 𝑥 ∈ V
2625inex1 4069 . . . . . . . 8 (𝑥𝐵) ∈ V
2726a1i 9 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝑥𝐵) ∈ V)
28 simpl1 985 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐾 ∈ (TopOn‘𝑌))
29 toponmax 12229 . . . . . . . . . 10 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
3028, 29syl 14 . . . . . . . . 9 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝑌𝐾)
31 simpl3 987 . . . . . . . . 9 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐵𝑌)
3230, 31ssexd 4075 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐵 ∈ V)
33 elrest 12164 . . . . . . . 8 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ V) → (𝑦 ∈ (𝐾t 𝐵) ↔ ∃𝑥𝐾 𝑦 = (𝑥𝐵)))
3428, 32, 33syl2anc 409 . . . . . . 7 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝑦 ∈ (𝐾t 𝐵) ↔ ∃𝑥𝐾 𝑦 = (𝑥𝐵)))
35 imaeq2 4884 . . . . . . . . 9 (𝑦 = (𝑥𝐵) → (𝐹𝑦) = (𝐹 “ (𝑥𝐵)))
3635eleq1d 2209 . . . . . . . 8 (𝑦 = (𝑥𝐵) → ((𝐹𝑦) ∈ 𝐽 ↔ (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
3736adantl 275 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑦 = (𝑥𝐵)) → ((𝐹𝑦) ∈ 𝐽 ↔ (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
3827, 34, 37ralxfr2d 4392 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽 ↔ ∀𝑥𝐾 (𝐹 “ (𝑥𝐵)) ∈ 𝐽))
39 simplrr 526 . . . . . . . . . 10 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → 𝐹: 𝐽𝐵)
40 ffun 5282 . . . . . . . . . 10 (𝐹: 𝐽𝐵 → Fun 𝐹)
41 inpreima 5553 . . . . . . . . . 10 (Fun 𝐹 → (𝐹 “ (𝑥𝐵)) = ((𝐹𝑥) ∩ (𝐹𝐵)))
4239, 40, 413syl 17 . . . . . . . . 9 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ (𝑥𝐵)) = ((𝐹𝑥) ∩ (𝐹𝐵)))
43 cnvimass 4909 . . . . . . . . . . . 12 (𝐹𝑥) ⊆ dom 𝐹
44 cnvimarndm 4910 . . . . . . . . . . . 12 (𝐹 “ ran 𝐹) = dom 𝐹
4543, 44sseqtrri 3136 . . . . . . . . . . 11 (𝐹𝑥) ⊆ (𝐹 “ ran 𝐹)
46 simpll2 1022 . . . . . . . . . . . 12 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ran 𝐹𝐵)
47 imass2 4922 . . . . . . . . . . . 12 (ran 𝐹𝐵 → (𝐹 “ ran 𝐹) ⊆ (𝐹𝐵))
4846, 47syl 14 . . . . . . . . . . 11 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ ran 𝐹) ⊆ (𝐹𝐵))
4945, 48sstrid 3112 . . . . . . . . . 10 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹𝑥) ⊆ (𝐹𝐵))
50 df-ss 3088 . . . . . . . . . 10 ((𝐹𝑥) ⊆ (𝐹𝐵) ↔ ((𝐹𝑥) ∩ (𝐹𝐵)) = (𝐹𝑥))
5149, 50sylib 121 . . . . . . . . 9 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ((𝐹𝑥) ∩ (𝐹𝐵)) = (𝐹𝑥))
5242, 51eqtrd 2173 . . . . . . . 8 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → (𝐹 “ (𝑥𝐵)) = (𝐹𝑥))
5352eleq1d 2209 . . . . . . 7 ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) ∧ 𝑥𝐾) → ((𝐹 “ (𝑥𝐵)) ∈ 𝐽 ↔ (𝐹𝑥) ∈ 𝐽))
5453ralbidva 2434 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑥𝐾 (𝐹 “ (𝑥𝐵)) ∈ 𝐽 ↔ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽))
55 simprr 522 . . . . . . . 8 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐹: 𝐽𝐵)
5655, 31fssd 5292 . . . . . . 7 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐹: 𝐽𝑌)
5756biantrurd 303 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽 ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
5838, 54, 573bitrrd 214 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → ((𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽) ↔ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽))
5955biantrurd 303 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽 ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6058, 59bitrd 187 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → ((𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
61 simprl 521 . . . . . 6 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐽 ∈ Top)
6261, 15sylib 121 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → 𝐽 ∈ (TopOn‘ 𝐽))
63 iscn 12403 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
6462, 28, 63syl2anc 409 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹: 𝐽𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
6518adantr 274 . . . . 5 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐾t 𝐵) ∈ (TopOn‘𝐵))
66 iscn 12403 . . . . 5 ((𝐽 ∈ (TopOn‘ 𝐽) ∧ (𝐾t 𝐵) ∈ (TopOn‘𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6762, 65, 66syl2anc 409 . . . 4 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)) ↔ (𝐹: 𝐽𝐵 ∧ ∀𝑦 ∈ (𝐾t 𝐵)(𝐹𝑦) ∈ 𝐽)))
6860, 64, 673bitr4d 219 . . 3 (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))))
6968ex 114 . 2 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → ((𝐽 ∈ Top ∧ 𝐹: 𝐽𝐵) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵)))))
7012, 24, 69pm5.21ndd 695 1 ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹𝐵𝐵𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾t 𝐵))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1332   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  Vcvv 2689   ∩ cin 3074   ⊆ wss 3075  ∪ cuni 3743  ◡ccnv 4545  dom cdm 4546  ran crn 4547   “ cima 4549  Fun wfun 5124   Fn wfn 5125  ⟶wf 5126  ‘cfv 5130  (class class class)co 5781   ↾t crest 12157  Topctop 12201  TopOnctopon 12214   Cn ccn 12391 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-id 4222  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-map 6551  df-rest 12159  df-topgen 12178  df-top 12202  df-topon 12215  df-bases 12247  df-cn 12394 This theorem is referenced by:  cnrest2r  12443  hmeores  12521
 Copyright terms: Public domain W3C validator