MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnrest2 Structured version   Visualization version   GIF version
Theorem cnrest2 22781
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 22735 . . . 4 (𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐽 ∈ Top)
21a1i 11 . . 3 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐽 ∈ Top))
3 eqid 2732 . . . . . . . 8 βˆͺ 𝐽 = βˆͺ 𝐽
4 eqid 2732 . . . . . . . 8 βˆͺ 𝐾 = βˆͺ 𝐾
53, 4cnf 22741 . . . . . . 7 (𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐹:βˆͺ 𝐽⟢βˆͺ 𝐾)
65ffnd 6715 . . . . . 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 6544 . . . 4 (𝐹:βˆͺ 𝐽⟢𝐡 ↔ (𝐹 Fn βˆͺ 𝐽 ∧ ran 𝐹 βŠ† 𝐡))
119, 10syl6ibr 251 . . 3 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐹:βˆͺ 𝐽⟢𝐡))
122, 11jcad 513 . 2 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) β†’ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)))
13 cntop1 22735 . . . . 5 (𝐹 ∈ (𝐽 Cn (𝐾 β†Ύt 𝐡)) β†’ 𝐽 ∈ Top)
1413adantl 482 . . . 4 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 β†Ύt 𝐡))) β†’ 𝐽 ∈ Top)
15 toptopon2 22411 . . . . . 6 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
1614, 15sylib 217 . . . . 5 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 β†Ύt 𝐡))) β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
17 resttopon 22656 . . . . . . 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 22744 . . . . 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 3478 . . . . . . . . 9 π‘₯ ∈ V
2625inex1 5316 . . . . . . . 8 (π‘₯ ∩ 𝐡) ∈ V
2726a1i 11 . . . . . . 7 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ (π‘₯ ∩ 𝐡) ∈ V)
28 simpl1 1191 . . . . . . . 8 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
29 toponmax 22419 . . . . . . . . . 10 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ π‘Œ ∈ 𝐾)
3028, 29syl 17 . . . . . . . . 9 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ π‘Œ ∈ 𝐾)
31 simpl3 1193 . . . . . . . . 9 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ 𝐡 βŠ† π‘Œ)
3230, 31ssexd 5323 . . . . . . . 8 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ 𝐡 ∈ V)
33 elrest 17369 . . . . . . . 8 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐡 ∈ V) β†’ (𝑦 ∈ (𝐾 β†Ύt 𝐡) ↔ βˆƒπ‘₯ ∈ 𝐾 𝑦 = (π‘₯ ∩ 𝐡)))
3428, 32, 33syl2anc 584 . . . . . . 7 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ (𝑦 ∈ (𝐾 β†Ύt 𝐡) ↔ βˆƒπ‘₯ ∈ 𝐾 𝑦 = (π‘₯ ∩ 𝐡)))
35 imaeq2 6053 . . . . . . . . 9 (𝑦 = (π‘₯ ∩ 𝐡) β†’ (◑𝐹 β€œ 𝑦) = (◑𝐹 β€œ (π‘₯ ∩ 𝐡)))
3635eleq1d 2818 . . . . . . . 8 (𝑦 = (π‘₯ ∩ 𝐡) β†’ ((◑𝐹 β€œ 𝑦) ∈ 𝐽 ↔ (◑𝐹 β€œ (π‘₯ ∩ 𝐡)) ∈ 𝐽))
3736adantl 482 . . . . . . 7 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ 𝑦 = (π‘₯ ∩ 𝐡)) β†’ ((◑𝐹 β€œ 𝑦) ∈ 𝐽 ↔ (◑𝐹 β€œ (π‘₯ ∩ 𝐡)) ∈ 𝐽))
3827, 34, 37ralxfr2d 5407 . . . . . 6 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ (βˆ€π‘¦ ∈ (𝐾 β†Ύt 𝐡)(◑𝐹 β€œ 𝑦) ∈ 𝐽 ↔ βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ (π‘₯ ∩ 𝐡)) ∈ 𝐽))
39 simplrr 776 . . . . . . . . . 10 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ 𝐹:βˆͺ 𝐽⟢𝐡)
40 ffun 6717 . . . . . . . . . 10 (𝐹:βˆͺ 𝐽⟢𝐡 β†’ Fun 𝐹)
41 inpreima 7062 . . . . . . . . . 10 (Fun 𝐹 β†’ (◑𝐹 β€œ (π‘₯ ∩ 𝐡)) = ((◑𝐹 β€œ π‘₯) ∩ (◑𝐹 β€œ 𝐡)))
4239, 40, 413syl 18 . . . . . . . . 9 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ (◑𝐹 β€œ (π‘₯ ∩ 𝐡)) = ((◑𝐹 β€œ π‘₯) ∩ (◑𝐹 β€œ 𝐡)))
43 cnvimass 6077 . . . . . . . . . . . 12 (◑𝐹 β€œ π‘₯) βŠ† dom 𝐹
44 cnvimarndm 6078 . . . . . . . . . . . 12 (◑𝐹 β€œ ran 𝐹) = dom 𝐹
4543, 44sseqtrri 4018 . . . . . . . . . . 11 (◑𝐹 β€œ π‘₯) βŠ† (◑𝐹 β€œ ran 𝐹)
46 simpll2 1213 . . . . . . . . . . . 12 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ ran 𝐹 βŠ† 𝐡)
47 imass2 6098 . . . . . . . . . . . 12 (ran 𝐹 βŠ† 𝐡 β†’ (◑𝐹 β€œ ran 𝐹) βŠ† (◑𝐹 β€œ 𝐡))
4846, 47syl 17 . . . . . . . . . . 11 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ (◑𝐹 β€œ ran 𝐹) βŠ† (◑𝐹 β€œ 𝐡))
4945, 48sstrid 3992 . . . . . . . . . 10 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ (◑𝐹 β€œ π‘₯) βŠ† (◑𝐹 β€œ 𝐡))
50 df-ss 3964 . . . . . . . . . 10 ((◑𝐹 β€œ π‘₯) βŠ† (◑𝐹 β€œ 𝐡) ↔ ((◑𝐹 β€œ π‘₯) ∩ (◑𝐹 β€œ 𝐡)) = (◑𝐹 β€œ π‘₯))
5149, 50sylib 217 . . . . . . . . 9 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ ((◑𝐹 β€œ π‘₯) ∩ (◑𝐹 β€œ 𝐡)) = (◑𝐹 β€œ π‘₯))
5242, 51eqtrd 2772 . . . . . . . 8 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ (◑𝐹 β€œ (π‘₯ ∩ 𝐡)) = (◑𝐹 β€œ π‘₯))
5352eleq1d 2818 . . . . . . 7 ((((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) ∧ π‘₯ ∈ 𝐾) β†’ ((◑𝐹 β€œ (π‘₯ ∩ 𝐡)) ∈ 𝐽 ↔ (◑𝐹 β€œ π‘₯) ∈ 𝐽))
5453ralbidva 3175 . . . . . 6 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ (βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ (π‘₯ ∩ 𝐡)) ∈ 𝐽 ↔ βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ π‘₯) ∈ 𝐽))
55 simprr 771 . . . . . . . 8 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ 𝐹:βˆͺ 𝐽⟢𝐡)
5655, 31fssd 6732 . . . . . . 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 22730 . . . . 5 ((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:βˆͺ π½βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
6462, 28, 63syl2anc 584 . . . 4 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:βˆͺ π½βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝐾 (◑𝐹 β€œ π‘₯) ∈ 𝐽)))
6518adantr 481 . . . . 5 (((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) ∧ (𝐽 ∈ Top ∧ 𝐹:βˆͺ 𝐽⟢𝐡)) β†’ (𝐾 β†Ύt 𝐡) ∈ (TopOnβ€˜π΅))
66 iscn 22730 . . . . 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 3061  βˆƒwrex 3070  Vcvv 3474   ∩ cin 3946   βŠ† wss 3947  βˆͺ cuni 4907  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   β†Ύt crest 17362  Topctop 22386  TopOnctopon 22403   Cn ccn 22719
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-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
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 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-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-map 8818  df-en 8936  df-fin 8939  df-fi 9402  df-rest 17364  df-topgen 17385  df-top 22387  df-topon 22404  df-bases 22440  df-cn 22722
This theorem is referenced by:  cnrest2r  22782  rncmp  22891  connima  22920  conncn  22921  kgencn2  23052  kgencn3  23053  qtoprest  23212  hmeores  23266  efmndtmd  23596  submtmd  23599  subgtgp  23600  symgtgp  23601  metdcn2  24346  metdscn2  24364  cnmptre  24434  iimulcn  24445  icchmeo  24448  evth  24466  evth2  24467  lebnumlem2  24469  reparphti  24504  efrlim  26463  rmulccn  32896  raddcn  32897  xrge0mulc1cn  32909  cvxpconn  34221  cvxsconn  34222  cvmliftmolem1  34260  cvmliftlem8  34271  cvmlift2lem9  34290  cvmlift3lem6  34303  gg-iimulcn  35157  gg-icchmeo  35158  gg-reparphti  35160  gg-rmulccn  35167  ivthALT  35208  knoppcnlem10  35366  broucube  36510  areacirclem2  36565  cnres2  36619  cnresima  36620  refsumcn  43699  icccncfext  44589
  Copyright terms: Public domain W3C validator