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

Theorem qtoprest 21761
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 6273 . . . . . . 7 (𝐹:𝑋onto𝑌𝐹 Fn 𝑋)
42, 3syl 17 . . . . . 6 (𝜑𝐹 Fn 𝑋)
5 qtopid 21749 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
61, 4, 5syl2anc 574 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)))
7 qtoprest.5 . . . . . . 7 (𝜑𝐴 = (𝐹𝑈))
8 cnvimass 5636 . . . . . . . 8 (𝐹𝑈) ⊆ dom 𝐹
9 fndm 6141 . . . . . . . . 9 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
104, 9syl 17 . . . . . . . 8 (𝜑 → dom 𝐹 = 𝑋)
118, 10syl5sseq 3809 . . . . . . 7 (𝜑 → (𝐹𝑈) ⊆ 𝑋)
127, 11eqsstrd 3795 . . . . . 6 (𝜑𝐴𝑋)
13 toponuni 20959 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
141, 13syl 17 . . . . . 6 (𝜑𝑋 = 𝐽)
1512, 14sseqtrd 3797 . . . . 5 (𝜑𝐴 𝐽)
16 eqid 2774 . . . . . 6 𝐽 = 𝐽
1716cnrest 21330 . . . . 5 ((𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)) ∧ 𝐴 𝐽) → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
186, 15, 17syl2anc 574 . . . 4 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)))
19 qtoptopon 21748 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
201, 2, 19syl2anc 574 . . . . 5 (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
21 df-ima 5276 . . . . . . 7 (𝐹𝐴) = ran (𝐹𝐴)
227imaeq2d 5617 . . . . . . . 8 (𝜑 → (𝐹𝐴) = (𝐹 “ (𝐹𝑈)))
23 qtoprest.4 . . . . . . . . 9 (𝜑𝑈𝑌)
24 foimacnv 6310 . . . . . . . . 9 ((𝐹:𝑋onto𝑌𝑈𝑌) → (𝐹 “ (𝐹𝑈)) = 𝑈)
252, 23, 24syl2anc 574 . . . . . . . 8 (𝜑 → (𝐹 “ (𝐹𝑈)) = 𝑈)
2622, 25eqtrd 2808 . . . . . . 7 (𝜑 → (𝐹𝐴) = 𝑈)
2721, 26syl5eqr 2822 . . . . . 6 (𝜑 → ran (𝐹𝐴) = 𝑈)
28 eqimss 3813 . . . . . 6 (ran (𝐹𝐴) = 𝑈 → ran (𝐹𝐴) ⊆ 𝑈)
2927, 28syl 17 . . . . 5 (𝜑 → ran (𝐹𝐴) ⊆ 𝑈)
30 cnrest2 21331 . . . . 5 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ ran (𝐹𝐴) ⊆ 𝑈𝑈𝑌) → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3120, 29, 23, 30syl3anc 1480 . . . 4 (𝜑 → ((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn (𝐽 qTop 𝐹)) ↔ (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈))))
3218, 31mpbid 223 . . 3 (𝜑 → (𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)))
33 resttopon 21206 . . . 4 (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝑈𝑌) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
3420, 23, 33syl2anc 574 . . 3 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
35 qtopss 21759 . . 3 (((𝐹𝐴) ∈ ((𝐽t 𝐴) Cn ((𝐽 qTop 𝐹) ↾t 𝑈)) ∧ ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) ∧ ran (𝐹𝐴) = 𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
3632, 34, 27, 35syl3anc 1480 . 2 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) ⊆ ((𝐽t 𝐴) qTop (𝐹𝐴)))
37 resttopon 21206 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴𝑋) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
381, 12, 37syl2anc 574 . . . . 5 (𝜑 → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
39 fnfun 6139 . . . . . . . 8 (𝐹 Fn 𝑋 → Fun 𝐹)
404, 39syl 17 . . . . . . 7 (𝜑 → Fun 𝐹)
4112, 10sseqtr4d 3798 . . . . . . 7 (𝜑𝐴 ⊆ dom 𝐹)
42 fores 6280 . . . . . . 7 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴):𝐴onto→(𝐹𝐴))
4340, 41, 42syl2anc 574 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴onto→(𝐹𝐴))
44 foeq3 6269 . . . . . . 7 ((𝐹𝐴) = 𝑈 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4526, 44syl 17 . . . . . 6 (𝜑 → ((𝐹𝐴):𝐴onto→(𝐹𝐴) ↔ (𝐹𝐴):𝐴onto𝑈))
4643, 45mpbid 223 . . . . 5 (𝜑 → (𝐹𝐴):𝐴onto𝑈)
47 elqtop3 21747 . . . . 5 (((𝐽t 𝐴) ∈ (TopOn‘𝐴) ∧ (𝐹𝐴):𝐴onto𝑈) → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
4838, 46, 47syl2anc 574 . . . 4 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) ↔ (𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴))))
49 cnvresima 5778 . . . . . . . 8 ((𝐹𝐴) “ 𝑥) = ((𝐹𝑥) ∩ 𝐴)
50 imass2 5652 . . . . . . . . . . 11 (𝑥𝑈 → (𝐹𝑥) ⊆ (𝐹𝑈))
5150adantl 468 . . . . . . . . . 10 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ (𝐹𝑈))
527adantr 467 . . . . . . . . . 10 ((𝜑𝑥𝑈) → 𝐴 = (𝐹𝑈))
5351, 52sseqtr4d 3798 . . . . . . . . 9 ((𝜑𝑥𝑈) → (𝐹𝑥) ⊆ 𝐴)
54 df-ss 3743 . . . . . . . . 9 ((𝐹𝑥) ⊆ 𝐴 ↔ ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5553, 54sylib 209 . . . . . . . 8 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∩ 𝐴) = (𝐹𝑥))
5649, 55syl5eq 2820 . . . . . . 7 ((𝜑𝑥𝑈) → ((𝐹𝐴) “ 𝑥) = (𝐹𝑥))
5756eleq1d 2838 . . . . . 6 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) ↔ (𝐹𝑥) ∈ (𝐽t 𝐴)))
58 simplrl 784 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑈)
59 df-ss 3743 . . . . . . . . . 10 (𝑥𝑈 ↔ (𝑥𝑈) = 𝑥)
6058, 59sylib 209 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) = 𝑥)
61 topontop 20958 . . . . . . . . . . . 12 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → (𝐽 qTop 𝐹) ∈ Top)
6220, 61syl 17 . . . . . . . . . . 11 (𝜑 → (𝐽 qTop 𝐹) ∈ Top)
6362ad2antrr 706 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐽 qTop 𝐹) ∈ Top)
64 toponmax 20971 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
651, 64syl 17 . . . . . . . . . . . . 13 (𝜑𝑋𝐽)
66 fornex 7303 . . . . . . . . . . . . 13 (𝑋𝐽 → (𝐹:𝑋onto𝑌𝑌 ∈ V))
6765, 2, 66sylc 65 . . . . . . . . . . . 12 (𝜑𝑌 ∈ V)
6867, 23ssexd 4953 . . . . . . . . . . 11 (𝜑𝑈 ∈ V)
6968ad2antrr 706 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈 ∈ V)
7023ad2antrr 706 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑈𝑌)
7158, 70sstrd 3768 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥𝑌)
72 topontop 20958 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
731, 72syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ Top)
74 restopn2 21222 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7573, 74sylan 570 . . . . . . . . . . . . . 14 ((𝜑𝐴𝐽) → ((𝐹𝑥) ∈ (𝐽t 𝐴) ↔ ((𝐹𝑥) ∈ 𝐽 ∧ (𝐹𝑥) ⊆ 𝐴)))
7675simprbda 487 . . . . . . . . . . . . 13 (((𝜑𝐴𝐽) ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → (𝐹𝑥) ∈ 𝐽)
7776adantrl 696 . . . . . . . . . . . 12 (((𝜑𝐴𝐽) ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐹𝑥) ∈ 𝐽)
7877an32s 632 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝐹𝑥) ∈ 𝐽)
79 elqtop3 21747 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
801, 2, 79syl2anc 574 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8180ad2antrr 706 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥𝑌 ∧ (𝐹𝑥) ∈ 𝐽)))
8271, 78, 81mpbir2and 693 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ (𝐽 qTop 𝐹))
83 elrestr 16317 . . . . . . . . . 10 (((𝐽 qTop 𝐹) ∈ Top ∧ 𝑈 ∈ V ∧ 𝑥 ∈ (𝐽 qTop 𝐹)) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8463, 69, 82, 83syl3anc 1480 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → (𝑥𝑈) ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8560, 84eqeltrrd 2854 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴𝐽) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
8634ad2antrr 706 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈))
87 toponuni 20959 . . . . . . . . . . . 12 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8886, 87syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 = ((𝐽 qTop 𝐹) ↾t 𝑈))
8988difeq1d 3885 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) = ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥))
9023ad2antrr 706 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈𝑌)
9120ad2antrr 706 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌))
92 toponuni 20959 . . . . . . . . . . . . 13 ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → 𝑌 = (𝐽 qTop 𝐹))
9391, 92syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑌 = (𝐽 qTop 𝐹))
9490, 93sseqtrd 3797 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑈 (𝐽 qTop 𝐹))
9590ssdifssd 3906 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑌)
9640ad2antrr 706 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → Fun 𝐹)
97 funcnvcnv 6107 . . . . . . . . . . . . . . 15 (Fun 𝐹 → Fun 𝐹)
98 imadif 6124 . . . . . . . . . . . . . . 15 (Fun 𝐹 → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
9996, 97, 983syl 18 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
1007ad2antrr 706 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐹𝑈))
101100difeq1d 3885 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ((𝐹𝑈) ∖ (𝐹𝑥)))
10299, 101eqtr4d 2811 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) = (𝐴 ∖ (𝐹𝑥)))
103 simpr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 ∈ (Clsd‘𝐽))
10438ad2antrr 706 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ (TopOn‘𝐴))
105 toponuni 20959 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → 𝐴 = (𝐽t 𝐴))
106104, 105syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝐴 = (𝐽t 𝐴))
107106difeq1d 3885 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) = ( (𝐽t 𝐴) ∖ (𝐹𝑥)))
108 topontop 20958 . . . . . . . . . . . . . . . . 17 ((𝐽t 𝐴) ∈ (TopOn‘𝐴) → (𝐽t 𝐴) ∈ Top)
109104, 108syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ Top)
110 simplrr 785 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹𝑥) ∈ (𝐽t 𝐴))
111 eqid 2774 . . . . . . . . . . . . . . . . 17 (𝐽t 𝐴) = (𝐽t 𝐴)
112111opncld 21078 . . . . . . . . . . . . . . . 16 (((𝐽t 𝐴) ∈ Top ∧ (𝐹𝑥) ∈ (𝐽t 𝐴)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
113109, 110, 112syl2anc 574 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( (𝐽t 𝐴) ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
114107, 113eqeltrd 2853 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴)))
115 restcldr 21219 . . . . . . . . . . . . . 14 ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘(𝐽t 𝐴))) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
116103, 114, 115syl2anc 574 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐴 ∖ (𝐹𝑥)) ∈ (Clsd‘𝐽))
117102, 116eqeltrd 2853 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))
118 qtopcld 21757 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋onto𝑌) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
1191, 2, 118syl2anc 574 . . . . . . . . . . . . 13 (𝜑 → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
120119ad2antrr 706 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ ((𝑈𝑥) ⊆ 𝑌 ∧ (𝐹 “ (𝑈𝑥)) ∈ (Clsd‘𝐽))))
12195, 117, 120mpbir2and 693 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)))
122 difssd 3896 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ⊆ 𝑈)
123 eqid 2774 . . . . . . . . . . . 12 (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)
124123restcldi 21218 . . . . . . . . . . 11 ((𝑈 (𝐽 qTop 𝐹) ∧ (𝑈𝑥) ∈ (Clsd‘(𝐽 qTop 𝐹)) ∧ (𝑈𝑥) ⊆ 𝑈) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12594, 121, 122, 124syl3anc 1480 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑈𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
12689, 125eqeltrrd 2854 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈)))
127 topontop 20958 . . . . . . . . . . 11 (((𝐽 qTop 𝐹) ↾t 𝑈) ∈ (TopOn‘𝑈) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
12886, 127syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top)
129 simplrl 784 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥𝑈)
130129, 88sseqtrd 3797 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈))
131 eqid 2774 . . . . . . . . . . 11 ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽 qTop 𝐹) ↾t 𝑈)
132131isopn2 21077 . . . . . . . . . 10 ((((𝐽 qTop 𝐹) ↾t 𝑈) ∈ Top ∧ 𝑥 ((𝐽 qTop 𝐹) ↾t 𝑈)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
133128, 130, 132syl2anc 574 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈) ↔ ( ((𝐽 qTop 𝐹) ↾t 𝑈) ∖ 𝑥) ∈ (Clsd‘((𝐽 qTop 𝐹) ↾t 𝑈))))
134126, 133mpbird 248 . . . . . . . 8 (((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) ∧ 𝐴 ∈ (Clsd‘𝐽)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
135 qtoprest.6 . . . . . . . . 9 (𝜑 → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
136135adantr 467 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → (𝐴𝐽𝐴 ∈ (Clsd‘𝐽)))
13785, 134, 136mpjaodan 970 . . . . . . 7 ((𝜑 ∧ (𝑥𝑈 ∧ (𝐹𝑥) ∈ (𝐽t 𝐴))) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈))
138137expr 445 . . . . . 6 ((𝜑𝑥𝑈) → ((𝐹𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
13957, 138sylbid 231 . . . . 5 ((𝜑𝑥𝑈) → (((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
140139expimpd 442 . . . 4 (𝜑 → ((𝑥𝑈 ∧ ((𝐹𝐴) “ 𝑥) ∈ (𝐽t 𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
14148, 140sylbid 231 . . 3 (𝜑 → (𝑥 ∈ ((𝐽t 𝐴) qTop (𝐹𝐴)) → 𝑥 ∈ ((𝐽 qTop 𝐹) ↾t 𝑈)))
142141ssrdv 3764 . 2 (𝜑 → ((𝐽t 𝐴) qTop (𝐹𝐴)) ⊆ ((𝐽 qTop 𝐹) ↾t 𝑈))
14336, 142eqssd 3775 1 (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽t 𝐴) qTop (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383  wo 863   = wceq 1634  wcel 2148  Vcvv 3355  cdif 3726  cin 3728  wss 3729   cuni 4585  ccnv 5262  dom cdm 5263  ran crn 5264  cres 5265  cima 5266  Fun wfun 6036   Fn wfn 6037  ontowfo 6040  cfv 6042  (class class class)co 6812  t crest 16309   qTop cqtop 16391  Topctop 20938  TopOnctopon 20955  Clsdccld 21061   Cn ccn 21269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-iin 4668  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-1st 7336  df-2nd 7337  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-oadd 7738  df-er 7917  df-map 8032  df-en 8131  df-fin 8134  df-fi 8494  df-rest 16311  df-topgen 16332  df-qtop 16395  df-top 20939  df-topon 20956  df-bases 20991  df-cld 21064  df-cn 21272
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator