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

Theorem qtoprest 22009
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 6460 . . . . . . 7 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
42, 3syl 17 . . . . . 6 (𝜑𝐹 Fn 𝑋)
5 qtopid 21997 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
61, 4, 5syl2anc 584 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
7 qtoprest.5 . . . . . . 7 (𝜑𝐴 = (𝐹𝑈))
8 cnvimass 5825 . . . . . . . 8 (𝐹𝑈) ⊆ dom 𝐹
9 fndm 6325 . . . . . . . . 9 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
104, 9syl 17 . . . . . . . 8 (𝜑 → dom 𝐹 = 𝑋)
118, 10sseqtrid 3940 . . . . . . 7 (𝜑 → (𝐹𝑈) ⊆ 𝑋)
127, 11eqsstrd 3926 . . . . . 6 (𝜑𝐴𝑋)
13 toponuni 21206 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
141, 13syl 17 . . . . . 6 (𝜑𝑋 = 𝐽)
1512, 14sseqtrd 3928 . . . . 5 (𝜑𝐴 𝐽)
16 eqid 2795 . . . . . 6 𝐽 = 𝐽
1716cnrest 21577 . . . . 5 ((𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)) ∧ 𝐴 𝐽) → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
186, 15, 17syl2anc 584 . . . 4 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
19 qtoptopon 21996 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
201, 2, 19syl2anc 584 . . . . 5 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
21 df-ima 5456 . . . . . . 7 (𝐹𝐴) = ran (𝐹𝐴)
227imaeq2d 5806 . . . . . . . 8 (𝜑 → (𝐹𝐴) = (𝐹 “ (𝐹𝑈)))
23 qtoprest.4 . . . . . . . . 9 (𝜑𝑈𝑌)
24 foimacnv 6500 . . . . . . . . 9 ((𝐹:𝑋onto𝑌𝑈𝑌) → (𝐹 “ (𝐹𝑈)) = 𝑈)
252, 23, 24syl2anc 584 . . . . . . . 8 (𝜑 → (𝐹 “ (𝐹𝑈)) = 𝑈)
2622, 25eqtrd 2831 . . . . . . 7 (𝜑 → (𝐹𝐴) = 𝑈)
2721, 26syl5eqr 2845 . . . . . 6 (𝜑 → ran (𝐹𝐴) = 𝑈)
28 eqimss 3944 . . . . . 6 (ran (𝐹𝐴) = 𝑈 → ran (𝐹𝐴) ⊆ 𝑈)
2927, 28syl 17 . . . . 5 (𝜑 → ran (𝐹𝐴) ⊆ 𝑈)
30 cnrest2 21578 . . . . 5 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ ran (𝐹𝐴) ⊆ 𝑈𝑈𝑌) → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3120, 29, 23, 30syl3anc 1364 . . . 4 (𝜑 → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3218, 31mpbid 233 . . 3 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)))
33 resttopon 21453 . . . 4 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝑈𝑌) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
3420, 23, 33syl2anc 584 . . 3 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
35 qtopss 22007 . . 3 (((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)) ∧ ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) ∧ ran (𝐹𝐴) = 𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
3632, 34, 27, 35syl3anc 1364 . 2 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
37 resttopon 21453 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴𝑋) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
381, 12, 37syl2anc 584 . . . . 5 (𝜑 → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
39 fnfun 6323 . . . . . . . 8 (𝐹 Fn 𝑋 → Fun 𝐹)
404, 39syl 17 . . . . . . 7 (𝜑 → Fun 𝐹)
4112, 10sseqtr4d 3929 . . . . . . 7 (𝜑𝐴 ⊆ dom 𝐹)
42 fores 6468 . . . . . . 7 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴):𝐴onto→(𝐹𝐴))
4340, 41, 42syl2anc 584 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴onto→(𝐹𝐴))
44 foeq3 6456 . . . . . . 7 ((𝐹𝐴) = 𝑈 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4526, 44syl 17 . . . . . 6 (𝜑 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4643, 45mpbid 233 . . . . 5 (𝜑 → (𝐹𝐴):𝐴onto𝑈)
47 elqtop3 21995 . . . . 5 (((𝐽t 𝐴) ∈ (TopOn‘𝐴) ∧ (𝐹𝐴):𝐴onto𝑈) → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
4838, 46, 47syl2anc 584 . . . 4 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
49 cnvresima 5962 . . . . . . . 8 ((𝐹𝐴) “ 𝑥) = ((𝐹𝑥) ∩ 𝐴)
50 imass2 5841 . . . . . . . . . . 11 (𝑥𝑈 → (𝐹𝑥) ⊆ (𝐹𝑈))
5150adantl 482 . . . . . . . . . 10 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ (𝐹𝑈))
527adantr 481 . . . . . . . . . 10 ((𝜑𝑥𝑈) → 𝐴 = (𝐹𝑈))
5351, 52sseqtr4d 3929 . . . . . . . . 9 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ 𝐴)
54 df-ss 3874 . . . . . . . . 9 ((𝐹𝑥) ⊆ 𝐴 ↔ ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5553, 54sylib 219 . . . . . . . 8 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5649, 55syl5eq 2843 . . . . . . 7 ((𝜑𝑥𝑈) → ((𝐹𝐴) “ 𝑥) = (𝐹𝑥))
5756eleq1d 2867 . . . . . 6 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) ↔ (𝐹𝑥) ∈ (𝐽t 𝐴)))
58 simplrl 773 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑈)
59 df-ss 3874 . . . . . . . . . 10 (𝑥𝑈 ↔ (𝑥𝑈) = 𝑥)
6058, 59sylib 219 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) = 𝑥)
61 topontop 21205 . . . . . . . . . . . 12 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → (𝐽 qTop 𝐹) ∈ Top)
6220, 61syl 17 . . . . . . . . . . 11 (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
6362ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐽 qTop 𝐹) ∈ Top)
64 toponmax 21218 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
651, 64syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝐽)
66 fornex 7513 . . . . . . . . . . . . 13 (𝑋𝐽 → (𝐹:𝑋onto𝑌𝑌 ∈ V))
6765, 2, 66sylc 65 . . . . . . . . . . . 12 (𝜑𝑌 ∈ V)
6867, 23ssexd 5119 . . . . . . . . . . 11 (𝜑𝑈 ∈ V)
6968ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈 ∈ V)
7023ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈𝑌)
7158, 70sstrd 3899 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑌)
72 topontop 21205 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
731, 72syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ Top)
74 restopn2 21469 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7573, 74sylan 580 . . . . . . . . . . . . . 14 ((𝜑𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7675simprbda 499 . . . . . . . . . . . . 13 (((𝜑𝐴𝐽) ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → (𝐹𝑥) ∈ 𝐽)
7776adantrl 712 . . . . . . . . . . . 12 (((𝜑𝐴𝐽) ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐹𝑥) ∈ 𝐽)
7877an32s 648 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐹𝑥) ∈ 𝐽)
79 elqtop3 21995 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
801, 2, 79syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8180ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8271, 78, 81mpbir2and 709 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ (𝐽 qTop 𝐹))
83 elrestr 16531 . . . . . . . . . 10 (((𝐽 qTop 𝐹) ∈ Top ∧ 𝑈 ∈ V ∧ 𝑥 ∈ (𝐽 qTop 𝐹)) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8463, 69, 82, 83syl3anc 1364 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8560, 84eqeltrrd 2884 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8634ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
87 toponuni 21206 . . . . . . . . . . . 12 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8886, 87syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8988difeq1d 4019 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) = ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥))
9023ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈𝑌)
9120ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
92 toponuni 21206 . . . . . . . . . . . . 13 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → 𝑌 = (𝐽 qTop 𝐹))
9391, 92syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑌 = (𝐽 qTop 𝐹))
9490, 93sseqtrd 3928 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 (𝐽 qTop 𝐹))
9590ssdifssd 4040 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑌)
9640ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → Fun 𝐹)
97 funcnvcnv 6291 . . . . . . . . . . . . . . 15 (Fun 𝐹 → Fun 𝐹)
98 imadif 6308 . . . . . . . . . . . . . . 15 (Fun 𝐹 → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
9996, 97, 983syl 18 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
1007ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐹𝑈))
101100difeq1d 4019 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
10299, 101eqtr4d 2834 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = (𝐴 ∖ (𝐹𝑥)))
103 simpr 485 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 ∈ (Clsd‘𝐽))
10438ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
105 toponuni 21206 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → 𝐴 = (𝐽t 𝐴))
106104, 105syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐽t 𝐴))
107106difeq1d 4019 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ( (𝐽t 𝐴) ∖ (𝐹𝑥)))
108 topontop 21205 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → (𝐽t 𝐴) ∈ Top)
109104, 108syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ Top)
110 simplrr 774 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹𝑥) ∈ (𝐽t 𝐴))
111 eqid 2795 . . . . . . . . . . . . . . . . 17 (𝐽t 𝐴) = (𝐽t 𝐴)
112111opncld 21325 . . . . . . . . . . . . . . . 16 (((𝐽t 𝐴) ∈ Top ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
113109, 110, 112syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
114107, 113eqeltrd 2883 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
115 restcldr 21466 . . . . . . . . . . . . . 14 ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴))) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
116103, 114, 115syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
117102, 116eqeltrd 2883 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))
118 qtopcld 22005 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
1191, 2, 118syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
120119ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
12195, 117, 120mpbir2and 709 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)))
122 difssd 4030 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑈)
123 eqid 2795 . . . . . . . . . . . 12 (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)
124123restcldi 21465 . . . . . . . . . . 11 ((𝑈 (𝐽 qTop 𝐹) ∧ (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ∧ (𝑈𝑥) ⊆ 𝑈) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12594, 121, 122, 124syl3anc 1364 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12689, 125eqeltrrd 2884 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
127 topontop 21205 . . . . . . . . . . 11 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
12886, 127syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
129 simplrl 773 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥𝑈)
130129, 88sseqtrd 3928 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈))
131 eqid 2795 . . . . . . . . . . 11 ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽 qTop 𝐹) ↾t 𝑈)
132131isopn2 21324 . . . . . . . . . 10 ((((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top ∧ 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
133128, 130, 132syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
134126, 133mpbird 258 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
135 qtoprest.6 . . . . . . . . 9 (𝜑 → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
136135adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
13785, 134, 136mpjaodan 953 . . . . . . 7 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
138137expr 457 . . . . . 6 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
13957, 138sylbid 241 . . . . 5 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
140139expimpd 454 . . . 4 (𝜑 → ((𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
14148, 140sylbid 241 . . 3 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
142141ssrdv 3895 . 2 (𝜑 → ((𝐽t 𝐴) qTop (𝐹𝐴)) ⊆ ((𝐽 qTop 𝐹) ↾t 𝑈))
14336, 142eqssd 3906 1 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽t 𝐴) qTop (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 842   = wceq 1522  wcel 2081  Vcvv 3437  cdif 3856  cin 3858  wss 3859   cuni 4745  ccnv 5442  dom cdm 5443  ran crn 5444  cres 5445  cima 5446  Fun wfun 6219   Fn wfn 6220  ontowfo 6223  cfv 6225  (class class class)co 7016  t crest 16523   qTop cqtop 16605  Topctop 21185  TopOnctopon 21202  Clsdccld 21308   Cn ccn 21516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-oadd 7957  df-er 8139  df-map 8258  df-en 8358  df-fin 8361  df-fi 8721  df-rest 16525  df-topgen 16546  df-qtop 16609  df-top 21186  df-topon 21203  df-bases 21238  df-cld 21311  df-cn 21519
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator