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

Theorem qtoprest 21568
Description: If 𝐴 is a saturated open or closed set (where saturated means that 𝐴 = (𝐹𝑈) for some 𝑈), then the restriction of the quotient map 𝐹 to 𝐴 is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
qtoprest.2 (𝜑𝐽 ∈ (TopOn‘𝑋))
qtoprest.3 (𝜑𝐹:𝑋onto𝑌)
qtoprest.4 (𝜑𝑈𝑌)
qtoprest.5 (𝜑𝐴 = (𝐹𝑈))
qtoprest.6 (𝜑 → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
Assertion
Ref Expression
qtoprest (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽t 𝐴) qTop (𝐹𝐴)))

Proof of Theorem qtoprest
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 qtoprest.2 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘𝑋))
2 qtoprest.3 . . . . . . 7 (𝜑𝐹:𝑋onto𝑌)
3 fofn 6155 . . . . . . 7 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
42, 3syl 17 . . . . . 6 (𝜑𝐹 Fn 𝑋)
5 qtopid 21556 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
61, 4, 5syl2anc 694 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
7 qtoprest.5 . . . . . . 7 (𝜑𝐴 = (𝐹𝑈))
8 cnvimass 5520 . . . . . . . 8 (𝐹𝑈) ⊆ dom 𝐹
9 fndm 6028 . . . . . . . . 9 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
104, 9syl 17 . . . . . . . 8 (𝜑 → dom 𝐹 = 𝑋)
118, 10syl5sseq 3686 . . . . . . 7 (𝜑 → (𝐹𝑈) ⊆ 𝑋)
127, 11eqsstrd 3672 . . . . . 6 (𝜑𝐴𝑋)
13 toponuni 20767 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
141, 13syl 17 . . . . . 6 (𝜑𝑋 = 𝐽)
1512, 14sseqtrd 3674 . . . . 5 (𝜑𝐴 𝐽)
16 eqid 2651 . . . . . 6 𝐽 = 𝐽
1716cnrest 21137 . . . . 5 ((𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)) ∧ 𝐴 𝐽) → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
186, 15, 17syl2anc 694 . . . 4 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
19 qtoptopon 21555 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
201, 2, 19syl2anc 694 . . . . 5 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
21 df-ima 5156 . . . . . . 7 (𝐹𝐴) = ran (𝐹𝐴)
227imaeq2d 5501 . . . . . . . 8 (𝜑 → (𝐹𝐴) = (𝐹 “ (𝐹𝑈)))
23 qtoprest.4 . . . . . . . . 9 (𝜑𝑈𝑌)
24 foimacnv 6192 . . . . . . . . 9 ((𝐹:𝑋onto𝑌𝑈𝑌) → (𝐹 “ (𝐹𝑈)) = 𝑈)
252, 23, 24syl2anc 694 . . . . . . . 8 (𝜑 → (𝐹 “ (𝐹𝑈)) = 𝑈)
2622, 25eqtrd 2685 . . . . . . 7 (𝜑 → (𝐹𝐴) = 𝑈)
2721, 26syl5eqr 2699 . . . . . 6 (𝜑 → ran (𝐹𝐴) = 𝑈)
28 eqimss 3690 . . . . . 6 (ran (𝐹𝐴) = 𝑈 → ran (𝐹𝐴) ⊆ 𝑈)
2927, 28syl 17 . . . . 5 (𝜑 → ran (𝐹𝐴) ⊆ 𝑈)
30 cnrest2 21138 . . . . 5 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ ran (𝐹𝐴) ⊆ 𝑈𝑈𝑌) → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3120, 29, 23, 30syl3anc 1366 . . . 4 (𝜑 → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3218, 31mpbid 222 . . 3 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)))
33 resttopon 21013 . . . 4 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝑈𝑌) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
3420, 23, 33syl2anc 694 . . 3 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
35 qtopss 21566 . . 3 (((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)) ∧ ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) ∧ ran (𝐹𝐴) = 𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
3632, 34, 27, 35syl3anc 1366 . 2 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
37 resttopon 21013 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴𝑋) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
381, 12, 37syl2anc 694 . . . . 5 (𝜑 → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
39 fnfun 6026 . . . . . . . 8 (𝐹 Fn 𝑋 → Fun 𝐹)
404, 39syl 17 . . . . . . 7 (𝜑 → Fun 𝐹)
4112, 10sseqtr4d 3675 . . . . . . 7 (𝜑𝐴 ⊆ dom 𝐹)
42 fores 6162 . . . . . . 7 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴):𝐴onto→(𝐹𝐴))
4340, 41, 42syl2anc 694 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴onto→(𝐹𝐴))
44 foeq3 6151 . . . . . . 7 ((𝐹𝐴) = 𝑈 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4526, 44syl 17 . . . . . 6 (𝜑 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4643, 45mpbid 222 . . . . 5 (𝜑 → (𝐹𝐴):𝐴onto𝑈)
47 elqtop3 21554 . . . . 5 (((𝐽t 𝐴) ∈ (TopOn‘𝐴) ∧ (𝐹𝐴):𝐴onto𝑈) → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
4838, 46, 47syl2anc 694 . . . 4 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
49 cnvresima 5661 . . . . . . . 8 ((𝐹𝐴) “ 𝑥) = ((𝐹𝑥) ∩ 𝐴)
50 imass2 5536 . . . . . . . . . . 11 (𝑥𝑈 → (𝐹𝑥) ⊆ (𝐹𝑈))
5150adantl 481 . . . . . . . . . 10 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ (𝐹𝑈))
527adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝑈) → 𝐴 = (𝐹𝑈))
5351, 52sseqtr4d 3675 . . . . . . . . 9 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ 𝐴)
54 df-ss 3621 . . . . . . . . 9 ((𝐹𝑥) ⊆ 𝐴 ↔ ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5553, 54sylib 208 . . . . . . . 8 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5649, 55syl5eq 2697 . . . . . . 7 ((𝜑𝑥𝑈) → ((𝐹𝐴) “ 𝑥) = (𝐹𝑥))
5756eleq1d 2715 . . . . . 6 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) ↔ (𝐹𝑥) ∈ (𝐽t 𝐴)))
58 simplrl 817 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑈)
59 df-ss 3621 . . . . . . . . . 10 (𝑥𝑈 ↔ (𝑥𝑈) = 𝑥)
6058, 59sylib 208 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) = 𝑥)
61 topontop 20766 . . . . . . . . . . . 12 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → (𝐽 qTop 𝐹) ∈ Top)
6220, 61syl 17 . . . . . . . . . . 11 (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
6362ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐽 qTop 𝐹) ∈ Top)
64 toponmax 20778 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
651, 64syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝐽)
66 fornex 7177 . . . . . . . . . . . . 13 (𝑋𝐽 → (𝐹:𝑋onto𝑌𝑌 ∈ V))
6765, 2, 66sylc 65 . . . . . . . . . . . 12 (𝜑𝑌 ∈ V)
6867, 23ssexd 4838 . . . . . . . . . . 11 (𝜑𝑈 ∈ V)
6968ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈 ∈ V)
7023ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈𝑌)
7158, 70sstrd 3646 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑌)
72 topontop 20766 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
731, 72syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ Top)
74 restopn2 21029 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7573, 74sylan 487 . . . . . . . . . . . . . 14 ((𝜑𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7675simprbda 652 . . . . . . . . . . . . 13 (((𝜑𝐴𝐽) ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → (𝐹𝑥) ∈ 𝐽)
7776adantrl 752 . . . . . . . . . . . 12 (((𝜑𝐴𝐽) ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐹𝑥) ∈ 𝐽)
7877an32s 863 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐹𝑥) ∈ 𝐽)
79 elqtop3 21554 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
801, 2, 79syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8180ad2antrr 762 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8271, 78, 81mpbir2and 977 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ (𝐽 qTop 𝐹))
83 elrestr 16136 . . . . . . . . . 10 (((𝐽 qTop 𝐹) ∈ Top ∧ 𝑈 ∈ V ∧ 𝑥 ∈ (𝐽 qTop 𝐹)) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8463, 69, 82, 83syl3anc 1366 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8560, 84eqeltrrd 2731 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8634ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
87 toponuni 20767 . . . . . . . . . . . 12 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8886, 87syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8988difeq1d 3760 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) = ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥))
9023ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈𝑌)
9120ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
92 toponuni 20767 . . . . . . . . . . . . 13 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → 𝑌 = (𝐽 qTop 𝐹))
9391, 92syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑌 = (𝐽 qTop 𝐹))
9490, 93sseqtrd 3674 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 (𝐽 qTop 𝐹))
9590ssdifssd 3781 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑌)
9640ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → Fun 𝐹)
97 funcnvcnv 5994 . . . . . . . . . . . . . . 15 (Fun 𝐹 → Fun 𝐹)
98 imadif 6011 . . . . . . . . . . . . . . 15 (Fun 𝐹 → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
9996, 97, 983syl 18 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
1007ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐹𝑈))
101100difeq1d 3760 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
10299, 101eqtr4d 2688 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = (𝐴 ∖ (𝐹𝑥)))
103 simpr 476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 ∈ (Clsd‘𝐽))
10438ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
105 toponuni 20767 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → 𝐴 = (𝐽t 𝐴))
106104, 105syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐽t 𝐴))
107106difeq1d 3760 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ( (𝐽t 𝐴) ∖ (𝐹𝑥)))
108 topontop 20766 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → (𝐽t 𝐴) ∈ Top)
109104, 108syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ Top)
110 simplrr 818 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹𝑥) ∈ (𝐽t 𝐴))
111 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝐽t 𝐴) = (𝐽t 𝐴)
112111opncld 20885 . . . . . . . . . . . . . . . 16 (((𝐽t 𝐴) ∈ Top ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
113109, 110, 112syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
114107, 113eqeltrd 2730 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
115 restcldr 21026 . . . . . . . . . . . . . 14 ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴))) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
116103, 114, 115syl2anc 694 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
117102, 116eqeltrd 2730 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))
118 qtopcld 21564 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
1191, 2, 118syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
120119ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
12195, 117, 120mpbir2and 977 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)))
122 difssd 3771 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑈)
123 eqid 2651 . . . . . . . . . . . 12 (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)
124123restcldi 21025 . . . . . . . . . . 11 ((𝑈 (𝐽 qTop 𝐹) ∧ (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ∧ (𝑈𝑥) ⊆ 𝑈) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12594, 121, 122, 124syl3anc 1366 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12689, 125eqeltrrd 2731 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
127 topontop 20766 . . . . . . . . . . 11 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
12886, 127syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
129 simplrl 817 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥𝑈)
130129, 88sseqtrd 3674 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈))
131 eqid 2651 . . . . . . . . . . 11 ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽 qTop 𝐹) ↾t 𝑈)
132131isopn2 20884 . . . . . . . . . 10 ((((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top ∧ 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
133128, 130, 132syl2anc 694 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
134126, 133mpbird 247 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
135 qtoprest.6 . . . . . . . . 9 (𝜑 → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
136135adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
13785, 134, 136mpjaodan 844 . . . . . . 7 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
138137expr 642 . . . . . 6 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
13957, 138sylbid 230 . . . . 5 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
140139expimpd 628 . . . 4 (𝜑 → ((𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
14148, 140sylbid 230 . . 3 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
142141ssrdv 3642 . 2 (𝜑 → ((𝐽t 𝐴) qTop (𝐹𝐴)) ⊆ ((𝐽 qTop 𝐹) ↾t 𝑈))
14336, 142eqssd 3653 1 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽t 𝐴) qTop (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  Vcvv 3231  cdif 3604  cin 3606  wss 3607   cuni 4468  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  Fun wfun 5920   Fn wfn 5921  ontowfo 5924  cfv 5926  (class class class)co 6690  t crest 16128   qTop cqtop 16210  Topctop 20746  TopOnctopon 20763  Clsdccld 20868   Cn ccn 21076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-fin 8001  df-fi 8358  df-rest 16130  df-topgen 16151  df-qtop 16214  df-top 20747  df-topon 20764  df-bases 20798  df-cld 20871  df-cn 21079
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator