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 dfss2 ⊢ ( ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝐴 ↔ ( ( ◡ 𝐹 “ 𝑥 ) ∩ 𝐴 ) = ( ◡ 𝐹 “ 𝑥 ) )
55 53 54 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑈 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∩ 𝐴 ) = ( ◡ 𝐹 “ 𝑥 ) )
56 49 55 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑈 ) → ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑥 ) = ( ◡ 𝐹 “ 𝑥 ) )
57 56 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑈 ) → ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑥 ) ∈ ( 𝐽 ↾t 𝐴 ) ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ ( 𝐽 ↾t 𝐴 ) ) )
58 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝑈 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ( 𝐽 ↾t 𝐴 ) ) ) ∧ 𝐴 ∈ 𝐽 ) → 𝑥 ⊆ 𝑈 )
59 dfss2 ⊢ ( 𝑥 ⊆ 𝑈 ↔ ( 𝑥 ∩ 𝑈 ) = 𝑥 )
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 focdmex ⊢ ( 𝑋 ∈ 𝐽 → ( 𝐹 : 𝑋 –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 ( 𝐹 ↾ 𝐴 ) ) )