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

Theorem qtoprest 21330
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 6030 . . . . . . 7 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
42, 3syl 17 . . . . . 6 (𝜑𝐹 Fn 𝑋)
5 qtopid 21318 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
61, 4, 5syl2anc 691 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
7 qtoprest.5 . . . . . . 7 (𝜑𝐴 = (𝐹𝑈))
8 cnvimass 5404 . . . . . . . 8 (𝐹𝑈) ⊆ dom 𝐹
9 fndm 5904 . . . . . . . . 9 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
104, 9syl 17 . . . . . . . 8 (𝜑 → dom 𝐹 = 𝑋)
118, 10syl5sseq 3616 . . . . . . 7 (𝜑 → (𝐹𝑈) ⊆ 𝑋)
127, 11eqsstrd 3602 . . . . . 6 (𝜑𝐴𝑋)
13 toponuni 20542 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
141, 13syl 17 . . . . . 6 (𝜑𝑋 = 𝐽)
1512, 14sseqtrd 3604 . . . . 5 (𝜑𝐴 𝐽)
16 eqid 2610 . . . . . 6 𝐽 = 𝐽
1716cnrest 20899 . . . . 5 ((𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)) ∧ 𝐴 𝐽) → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
186, 15, 17syl2anc 691 . . . 4 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
19 qtoptopon 21317 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
201, 2, 19syl2anc 691 . . . . 5 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
21 df-ima 5051 . . . . . . 7 (𝐹𝐴) = ran (𝐹𝐴)
227imaeq2d 5385 . . . . . . . 8 (𝜑 → (𝐹𝐴) = (𝐹 “ (𝐹𝑈)))
23 qtoprest.4 . . . . . . . . 9 (𝜑𝑈𝑌)
24 foimacnv 6067 . . . . . . . . 9 ((𝐹:𝑋onto𝑌𝑈𝑌) → (𝐹 “ (𝐹𝑈)) = 𝑈)
252, 23, 24syl2anc 691 . . . . . . . 8 (𝜑 → (𝐹 “ (𝐹𝑈)) = 𝑈)
2622, 25eqtrd 2644 . . . . . . 7 (𝜑 → (𝐹𝐴) = 𝑈)
2721, 26syl5eqr 2658 . . . . . 6 (𝜑 → ran (𝐹𝐴) = 𝑈)
28 eqimss 3620 . . . . . 6 (ran (𝐹𝐴) = 𝑈 → ran (𝐹𝐴) ⊆ 𝑈)
2927, 28syl 17 . . . . 5 (𝜑 → ran (𝐹𝐴) ⊆ 𝑈)
30 cnrest2 20900 . . . . 5 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ ran (𝐹𝐴) ⊆ 𝑈𝑈𝑌) → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3120, 29, 23, 30syl3anc 1318 . . . 4 (𝜑 → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3218, 31mpbid 221 . . 3 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)))
33 resttopon 20775 . . . 4 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝑈𝑌) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
3420, 23, 33syl2anc 691 . . 3 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
35 qtopss 21328 . . 3 (((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)) ∧ ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) ∧ ran (𝐹𝐴) = 𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
3632, 34, 27, 35syl3anc 1318 . 2 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
37 resttopon 20775 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴𝑋) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
381, 12, 37syl2anc 691 . . . . 5 (𝜑 → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
39 fnfun 5902 . . . . . . . 8 (𝐹 Fn 𝑋 → Fun 𝐹)
404, 39syl 17 . . . . . . 7 (𝜑 → Fun 𝐹)
4112, 10sseqtr4d 3605 . . . . . . 7 (𝜑𝐴 ⊆ dom 𝐹)
42 fores 6037 . . . . . . 7 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴):𝐴onto→(𝐹𝐴))
4340, 41, 42syl2anc 691 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴onto→(𝐹𝐴))
44 foeq3 6026 . . . . . . 7 ((𝐹𝐴) = 𝑈 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4526, 44syl 17 . . . . . 6 (𝜑 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4643, 45mpbid 221 . . . . 5 (𝜑 → (𝐹𝐴):𝐴onto𝑈)
47 elqtop3 21316 . . . . 5 (((𝐽t 𝐴) ∈ (TopOn‘𝐴) ∧ (𝐹𝐴):𝐴onto𝑈) → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
4838, 46, 47syl2anc 691 . . . 4 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
49 cnvresima 5541 . . . . . . . 8 ((𝐹𝐴) “ 𝑥) = ((𝐹𝑥) ∩ 𝐴)
50 imass2 5420 . . . . . . . . . . 11 (𝑥𝑈 → (𝐹𝑥) ⊆ (𝐹𝑈))
5150adantl 481 . . . . . . . . . 10 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ (𝐹𝑈))
527adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝑈) → 𝐴 = (𝐹𝑈))
5351, 52sseqtr4d 3605 . . . . . . . . 9 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ 𝐴)
54 df-ss 3554 . . . . . . . . 9 ((𝐹𝑥) ⊆ 𝐴 ↔ ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5553, 54sylib 207 . . . . . . . 8 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5649, 55syl5eq 2656 . . . . . . 7 ((𝜑𝑥𝑈) → ((𝐹𝐴) “ 𝑥) = (𝐹𝑥))
5756eleq1d 2672 . . . . . 6 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) ↔ (𝐹𝑥) ∈ (𝐽t 𝐴)))
58 simplrl 796 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑈)
59 df-ss 3554 . . . . . . . . . 10 (𝑥𝑈 ↔ (𝑥𝑈) = 𝑥)
6058, 59sylib 207 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) = 𝑥)
61 topontop 20541 . . . . . . . . . . . 12 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → (𝐽 qTop 𝐹) ∈ Top)
6220, 61syl 17 . . . . . . . . . . 11 (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
6362ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐽 qTop 𝐹) ∈ Top)
64 toponmax 20543 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
651, 64syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝐽)
66 fornex 7028 . . . . . . . . . . . . 13 (𝑋𝐽 → (𝐹:𝑋onto𝑌𝑌 ∈ V))
6765, 2, 66sylc 63 . . . . . . . . . . . 12 (𝜑𝑌 ∈ V)
6867, 23ssexd 4733 . . . . . . . . . . 11 (𝜑𝑈 ∈ V)
6968ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈 ∈ V)
7023ad2antrr 758 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈𝑌)
7158, 70sstrd 3578 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑌)
72 topontop 20541 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
731, 72syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ Top)
74 restopn2 20791 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7573, 74sylan 487 . . . . . . . . . . . . . 14 ((𝜑𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7675simprbda 651 . . . . . . . . . . . . 13 (((𝜑𝐴𝐽) ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → (𝐹𝑥) ∈ 𝐽)
7776adantrl 748 . . . . . . . . . . . 12 (((𝜑𝐴𝐽) ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐹𝑥) ∈ 𝐽)
7877an32s 842 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐹𝑥) ∈ 𝐽)
79 elqtop3 21316 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
801, 2, 79syl2anc 691 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8180ad2antrr 758 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8271, 78, 81mpbir2and 959 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ (𝐽 qTop 𝐹))
83 elrestr 15912 . . . . . . . . . 10 (((𝐽 qTop 𝐹) ∈ Top ∧ 𝑈 ∈ V ∧ 𝑥 ∈ (𝐽 qTop 𝐹)) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8463, 69, 82, 83syl3anc 1318 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8560, 84eqeltrrd 2689 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8634ad2antrr 758 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
87 toponuni 20542 . . . . . . . . . . . 12 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8886, 87syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8988difeq1d 3689 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) = ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥))
9023ad2antrr 758 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈𝑌)
9120ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
92 toponuni 20542 . . . . . . . . . . . . 13 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → 𝑌 = (𝐽 qTop 𝐹))
9391, 92syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑌 = (𝐽 qTop 𝐹))
9490, 93sseqtrd 3604 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 (𝐽 qTop 𝐹))
9590ssdifssd 3710 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑌)
9640ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → Fun 𝐹)
97 funcnvcnv 5870 . . . . . . . . . . . . . . 15 (Fun 𝐹 → Fun 𝐹)
98 imadif 5887 . . . . . . . . . . . . . . 15 (Fun 𝐹 → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
9996, 97, 983syl 18 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
1007ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐹𝑈))
101100difeq1d 3689 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
10299, 101eqtr4d 2647 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = (𝐴 ∖ (𝐹𝑥)))
103 simpr 476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 ∈ (Clsd‘𝐽))
10438ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
105 toponuni 20542 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → 𝐴 = (𝐽t 𝐴))
106104, 105syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐽t 𝐴))
107106difeq1d 3689 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ( (𝐽t 𝐴) ∖ (𝐹𝑥)))
108 topontop 20541 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → (𝐽t 𝐴) ∈ Top)
109104, 108syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ Top)
110 simplrr 797 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹𝑥) ∈ (𝐽t 𝐴))
111 eqid 2610 . . . . . . . . . . . . . . . . 17 (𝐽t 𝐴) = (𝐽t 𝐴)
112111opncld 20647 . . . . . . . . . . . . . . . 16 (((𝐽t 𝐴) ∈ Top ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
113109, 110, 112syl2anc 691 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
114107, 113eqeltrd 2688 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
115 restcldr 20788 . . . . . . . . . . . . . 14 ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴))) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
116103, 114, 115syl2anc 691 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
117102, 116eqeltrd 2688 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))
118 qtopcld 21326 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
1191, 2, 118syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
120119ad2antrr 758 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
12195, 117, 120mpbir2and 959 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)))
122 difssd 3700 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑈)
123 eqid 2610 . . . . . . . . . . . 12 (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)
124123restcldi 20787 . . . . . . . . . . 11 ((𝑈 (𝐽 qTop 𝐹) ∧ (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ∧ (𝑈𝑥) ⊆ 𝑈) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12594, 121, 122, 124syl3anc 1318 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12689, 125eqeltrrd 2689 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
127 topontop 20541 . . . . . . . . . . 11 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
12886, 127syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
129 simplrl 796 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥𝑈)
130129, 88sseqtrd 3604 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈))
131 eqid 2610 . . . . . . . . . . 11 ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽 qTop 𝐹) ↾t 𝑈)
132131isopn2 20646 . . . . . . . . . 10 ((((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top ∧ 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
133128, 130, 132syl2anc 691 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
134126, 133mpbird 246 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
135 qtoprest.6 . . . . . . . . 9 (𝜑 → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
136135adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
13785, 134, 136mpjaodan 823 . . . . . . 7 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
138137expr 641 . . . . . 6 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
13957, 138sylbid 229 . . . . 5 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
140139expimpd 627 . . . 4 (𝜑 → ((𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
14148, 140sylbid 229 . . 3 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
142141ssrdv 3574 . 2 (𝜑 → ((𝐽t 𝐴) qTop (𝐹𝐴)) ⊆ ((𝐽 qTop 𝐹) ↾t 𝑈))
14336, 142eqssd 3585 1 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽t 𝐴) qTop (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wo 382  wa 383   = wceq 1475  wcel 1977  Vcvv 3173  cdif 3537  cin 3539  wss 3540   cuni 4372  ccnv 5037  dom cdm 5038  ran crn 5039  cres 5040  cima 5041  Fun wfun 5798   Fn wfn 5799  ontowfo 5802  cfv 5804  (class class class)co 6549  t crest 15904   qTop cqtop 15986  Topctop 20517  TopOnctopon 20518  Clsdccld 20630   Cn ccn 20838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-qtop 15990  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-cn 20841
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator