Metamath Proof Explorer


Theorem qtoprest

Description: If A is a saturated open or closed set (where saturated means that A = (`' F " U ) for some U ), then the restriction of the quotient map F to A ` is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses qtoprest.2 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
qtoprest.3 ( 𝜑𝐹 : 𝑋onto𝑌 )
qtoprest.4 ( 𝜑𝑈𝑌 )
qtoprest.5 ( 𝜑𝐴 = ( 𝐹𝑈 ) )
qtoprest.6 ( 𝜑 → ( 𝐴𝐽𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
Assertion qtoprest ( 𝜑 → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) = ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 qtoprest.2 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 qtoprest.3 ( 𝜑𝐹 : 𝑋onto𝑌 )
3 qtoprest.4 ( 𝜑𝑈𝑌 )
4 qtoprest.5 ( 𝜑𝐴 = ( 𝐹𝑈 ) )
5 qtoprest.6 ( 𝜑 → ( 𝐴𝐽𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
6 fofn ( 𝐹 : 𝑋onto𝑌𝐹 Fn 𝑋 )
7 2 6 syl ( 𝜑𝐹 Fn 𝑋 )
8 qtopid ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
9 1 7 8 syl2anc ( 𝜑𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
10 cnvimass ( 𝐹𝑈 ) ⊆ dom 𝐹
11 7 fndmd ( 𝜑 → dom 𝐹 = 𝑋 )
12 10 11 sseqtrid ( 𝜑 → ( 𝐹𝑈 ) ⊆ 𝑋 )
13 4 12 eqsstrd ( 𝜑𝐴𝑋 )
14 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
15 1 14 syl ( 𝜑𝑋 = 𝐽 )
16 13 15 sseqtrd ( 𝜑𝐴 𝐽 )
17 eqid 𝐽 = 𝐽
18 17 cnrest ( ( 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐴 𝐽 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( 𝐽 qTop 𝐹 ) ) )
19 9 16 18 syl2anc ( 𝜑 → ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( 𝐽 qTop 𝐹 ) ) )
20 qtoptopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
21 1 2 20 syl2anc ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
22 df-ima ( 𝐹𝐴 ) = ran ( 𝐹𝐴 )
23 4 imaeq2d ( 𝜑 → ( 𝐹𝐴 ) = ( 𝐹 “ ( 𝐹𝑈 ) ) )
24 foimacnv ( ( 𝐹 : 𝑋onto𝑌𝑈𝑌 ) → ( 𝐹 “ ( 𝐹𝑈 ) ) = 𝑈 )
25 2 3 24 syl2anc ( 𝜑 → ( 𝐹 “ ( 𝐹𝑈 ) ) = 𝑈 )
26 23 25 eqtrd ( 𝜑 → ( 𝐹𝐴 ) = 𝑈 )
27 22 26 eqtr3id ( 𝜑 → ran ( 𝐹𝐴 ) = 𝑈 )
28 eqimss ( ran ( 𝐹𝐴 ) = 𝑈 → ran ( 𝐹𝐴 ) ⊆ 𝑈 )
29 27 28 syl ( 𝜑 → ran ( 𝐹𝐴 ) ⊆ 𝑈 )
30 cnrest2 ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ran ( 𝐹𝐴 ) ⊆ 𝑈𝑈𝑌 ) → ( ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) ) )
31 21 29 3 30 syl3anc ( 𝜑 → ( ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) ) )
32 19 31 mpbid ( 𝜑 → ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
33 resttopon ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑈𝑌 ) → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
34 21 3 33 syl2anc ( 𝜑 → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
35 qtopss ( ( ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) ∧ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) ∧ ran ( 𝐹𝐴 ) = 𝑈 ) → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ⊆ ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) )
36 32 34 27 35 syl3anc ( 𝜑 → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ⊆ ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) )
37 resttopon ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴𝑋 ) → ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
38 1 13 37 syl2anc ( 𝜑 → ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
39 fnfun ( 𝐹 Fn 𝑋 → Fun 𝐹 )
40 7 39 syl ( 𝜑 → Fun 𝐹 )
41 13 11 sseqtrrd ( 𝜑𝐴 ⊆ dom 𝐹 )
42 fores ( ( Fun 𝐹𝐴 ⊆ dom 𝐹 ) → ( 𝐹𝐴 ) : 𝐴onto→ ( 𝐹𝐴 ) )
43 40 41 42 syl2anc ( 𝜑 → ( 𝐹𝐴 ) : 𝐴onto→ ( 𝐹𝐴 ) )
44 foeq3 ( ( 𝐹𝐴 ) = 𝑈 → ( ( 𝐹𝐴 ) : 𝐴onto→ ( 𝐹𝐴 ) ↔ ( 𝐹𝐴 ) : 𝐴onto𝑈 ) )
45 26 44 syl ( 𝜑 → ( ( 𝐹𝐴 ) : 𝐴onto→ ( 𝐹𝐴 ) ↔ ( 𝐹𝐴 ) : 𝐴onto𝑈 ) )
46 43 45 mpbid ( 𝜑 → ( 𝐹𝐴 ) : 𝐴onto𝑈 )
47 elqtop3 ( ( ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ ( 𝐹𝐴 ) : 𝐴onto𝑈 ) → ( 𝑥 ∈ ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) ↔ ( 𝑥𝑈 ∧ ( ( 𝐹𝐴 ) “ 𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) )
48 38 46 47 syl2anc ( 𝜑 → ( 𝑥 ∈ ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) ↔ ( 𝑥𝑈 ∧ ( ( 𝐹𝐴 ) “ 𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) )
49 cnvresima ( ( 𝐹𝐴 ) “ 𝑥 ) = ( ( 𝐹𝑥 ) ∩ 𝐴 )
50 imass2 ( 𝑥𝑈 → ( 𝐹𝑥 ) ⊆ ( 𝐹𝑈 ) )
51 50 adantl ( ( 𝜑𝑥𝑈 ) → ( 𝐹𝑥 ) ⊆ ( 𝐹𝑈 ) )
52 4 adantr ( ( 𝜑𝑥𝑈 ) → 𝐴 = ( 𝐹𝑈 ) )
53 51 52 sseqtrrd ( ( 𝜑𝑥𝑈 ) → ( 𝐹𝑥 ) ⊆ 𝐴 )
54 df-ss ( ( 𝐹𝑥 ) ⊆ 𝐴 ↔ ( ( 𝐹𝑥 ) ∩ 𝐴 ) = ( 𝐹𝑥 ) )
55 53 54 sylib ( ( 𝜑𝑥𝑈 ) → ( ( 𝐹𝑥 ) ∩ 𝐴 ) = ( 𝐹𝑥 ) )
56 49 55 syl5eq ( ( 𝜑𝑥𝑈 ) → ( ( 𝐹𝐴 ) “ 𝑥 ) = ( 𝐹𝑥 ) )
57 56 eleq1d ( ( 𝜑𝑥𝑈 ) → ( ( ( 𝐹𝐴 ) “ 𝑥 ) ∈ ( 𝐽t 𝐴 ) ↔ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) )
58 simplrl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → 𝑥𝑈 )
59 df-ss ( 𝑥𝑈 ↔ ( 𝑥𝑈 ) = 𝑥 )
60 58 59 sylib ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → ( 𝑥𝑈 ) = 𝑥 )
61 topontop ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
62 21 61 syl ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ Top )
63 62 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )
64 toponmax ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋𝐽 )
65 1 64 syl ( 𝜑𝑋𝐽 )
66 fornex ( 𝑋𝐽 → ( 𝐹 : 𝑋onto𝑌𝑌 ∈ V ) )
67 65 2 66 sylc ( 𝜑𝑌 ∈ V )
68 67 3 ssexd ( 𝜑𝑈 ∈ V )
69 68 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → 𝑈 ∈ V )
70 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → 𝑈𝑌 )
71 58 70 sstrd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → 𝑥𝑌 )
72 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
73 1 72 syl ( 𝜑𝐽 ∈ Top )
74 restopn2 ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → ( ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ↔ ( ( 𝐹𝑥 ) ∈ 𝐽 ∧ ( 𝐹𝑥 ) ⊆ 𝐴 ) ) )
75 73 74 sylan ( ( 𝜑𝐴𝐽 ) → ( ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ↔ ( ( 𝐹𝑥 ) ∈ 𝐽 ∧ ( 𝐹𝑥 ) ⊆ 𝐴 ) ) )
76 75 simprbda ( ( ( 𝜑𝐴𝐽 ) ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) → ( 𝐹𝑥 ) ∈ 𝐽 )
77 76 adantrl ( ( ( 𝜑𝐴𝐽 ) ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) → ( 𝐹𝑥 ) ∈ 𝐽 )
78 77 an32s ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → ( 𝐹𝑥 ) ∈ 𝐽 )
79 elqtop3 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋onto𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥𝑌 ∧ ( 𝐹𝑥 ) ∈ 𝐽 ) ) )
80 1 2 79 syl2anc ( 𝜑 → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥𝑌 ∧ ( 𝐹𝑥 ) ∈ 𝐽 ) ) )
81 80 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥𝑌 ∧ ( 𝐹𝑥 ) ∈ 𝐽 ) ) )
82 71 78 81 mpbir2and ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → 𝑥 ∈ ( 𝐽 qTop 𝐹 ) )
83 elrestr ( ( ( 𝐽 qTop 𝐹 ) ∈ Top ∧ 𝑈 ∈ V ∧ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ) → ( 𝑥𝑈 ) ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
84 63 69 82 83 syl3anc ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → ( 𝑥𝑈 ) ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
85 60 84 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴𝐽 ) → 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
86 34 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) )
87 toponuni ( ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) → 𝑈 = ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
88 86 87 syl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 = ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
89 88 difeq1d ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈𝑥 ) = ( ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∖ 𝑥 ) )
90 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈𝑌 )
91 21 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
92 toponuni ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ( 𝐽 qTop 𝐹 ) )
93 91 92 syl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑌 = ( 𝐽 qTop 𝐹 ) )
94 90 93 sseqtrd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑈 ( 𝐽 qTop 𝐹 ) )
95 90 ssdifssd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈𝑥 ) ⊆ 𝑌 )
96 40 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → Fun 𝐹 )
97 funcnvcnv ( Fun 𝐹 → Fun 𝐹 )
98 imadif ( Fun 𝐹 → ( 𝐹 “ ( 𝑈𝑥 ) ) = ( ( 𝐹𝑈 ) ∖ ( 𝐹𝑥 ) ) )
99 96 97 98 3syl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ ( 𝑈𝑥 ) ) = ( ( 𝐹𝑈 ) ∖ ( 𝐹𝑥 ) ) )
100 4 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐴 = ( 𝐹𝑈 ) )
101 100 difeq1d ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ( ( 𝐹𝑈 ) ∖ ( 𝐹𝑥 ) ) )
102 99 101 eqtr4d ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ ( 𝑈𝑥 ) ) = ( 𝐴 ∖ ( 𝐹𝑥 ) ) )
103 simpr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )
104 38 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
105 toponuni ( ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) → 𝐴 = ( 𝐽t 𝐴 ) )
106 104 105 syl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐴 = ( 𝐽t 𝐴 ) )
107 106 difeq1d ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∖ ( 𝐹𝑥 ) ) = ( ( 𝐽t 𝐴 ) ∖ ( 𝐹𝑥 ) ) )
108 topontop ( ( 𝐽t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) → ( 𝐽t 𝐴 ) ∈ Top )
109 104 108 syl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽t 𝐴 ) ∈ Top )
110 simplrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) )
111 eqid ( 𝐽t 𝐴 ) = ( 𝐽t 𝐴 )
112 111 opncld ( ( ( 𝐽t 𝐴 ) ∈ Top ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) → ( ( 𝐽t 𝐴 ) ∖ ( 𝐹𝑥 ) ) ∈ ( Clsd ‘ ( 𝐽t 𝐴 ) ) )
113 109 110 112 syl2anc ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐽t 𝐴 ) ∖ ( 𝐹𝑥 ) ) ∈ ( Clsd ‘ ( 𝐽t 𝐴 ) ) )
114 107 113 eqeltrd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∖ ( 𝐹𝑥 ) ) ∈ ( Clsd ‘ ( 𝐽t 𝐴 ) ) )
115 restcldr ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐴 ∖ ( 𝐹𝑥 ) ) ∈ ( Clsd ‘ ( 𝐽t 𝐴 ) ) ) → ( 𝐴 ∖ ( 𝐹𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
116 103 114 115 syl2anc ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∖ ( 𝐹𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
117 102 116 eqeltrd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐹 “ ( 𝑈𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) )
118 qtopcld ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋onto𝑌 ) → ( ( 𝑈𝑥 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝑈𝑥 ) ⊆ 𝑌 ∧ ( 𝐹 “ ( 𝑈𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
119 1 2 118 syl2anc ( 𝜑 → ( ( 𝑈𝑥 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝑈𝑥 ) ⊆ 𝑌 ∧ ( 𝐹 “ ( 𝑈𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
120 119 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑈𝑥 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝑈𝑥 ) ⊆ 𝑌 ∧ ( 𝐹 “ ( 𝑈𝑥 ) ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
121 95 117 120 mpbir2and ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈𝑥 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) )
122 difssd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈𝑥 ) ⊆ 𝑈 )
123 eqid ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop 𝐹 )
124 123 restcldi ( ( 𝑈 ( 𝐽 qTop 𝐹 ) ∧ ( 𝑈𝑥 ) ∈ ( Clsd ‘ ( 𝐽 qTop 𝐹 ) ) ∧ ( 𝑈𝑥 ) ⊆ 𝑈 ) → ( 𝑈𝑥 ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
125 94 121 122 124 syl3anc ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑈𝑥 ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
126 89 125 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∖ 𝑥 ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
127 topontop ( ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ ( TopOn ‘ 𝑈 ) → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ Top )
128 86 127 syl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ Top )
129 simplrl ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥𝑈 )
130 129 88 sseqtrd ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
131 eqid ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) = ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 )
132 131 isopn2 ( ( ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∈ Top ∧ 𝑥 ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) → ( 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ↔ ( ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∖ 𝑥 ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) ) )
133 128 130 132 syl2anc ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ↔ ( ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ∖ 𝑥 ) ∈ ( Clsd ‘ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) ) )
134 126 133 mpbird ( ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
135 5 adantr ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) → ( 𝐴𝐽𝐴 ∈ ( Clsd ‘ 𝐽 ) ) )
136 85 134 135 mpjaodan ( ( 𝜑 ∧ ( 𝑥𝑈 ∧ ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) ) ) → 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
137 136 expr ( ( 𝜑𝑥𝑈 ) → ( ( 𝐹𝑥 ) ∈ ( 𝐽t 𝐴 ) → 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
138 57 137 sylbid ( ( 𝜑𝑥𝑈 ) → ( ( ( 𝐹𝐴 ) “ 𝑥 ) ∈ ( 𝐽t 𝐴 ) → 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
139 138 expimpd ( 𝜑 → ( ( 𝑥𝑈 ∧ ( ( 𝐹𝐴 ) “ 𝑥 ) ∈ ( 𝐽t 𝐴 ) ) → 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
140 48 139 sylbid ( 𝜑 → ( 𝑥 ∈ ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) → 𝑥 ∈ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) ) )
141 140 ssrdv ( 𝜑 → ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) ⊆ ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) )
142 36 141 eqssd ( 𝜑 → ( ( 𝐽 qTop 𝐹 ) ↾t 𝑈 ) = ( ( 𝐽t 𝐴 ) qTop ( 𝐹𝐴 ) ) )