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 
|- ( ph -> J e. ( TopOn ` X ) )
qtoprest.3 
|- ( ph -> F : X -onto-> Y )
qtoprest.4 
|- ( ph -> U C_ Y )
qtoprest.5 
|- ( ph -> A = ( `' F " U ) )
qtoprest.6 
|- ( ph -> ( A e. J \/ A e. ( Clsd ` J ) ) )
Assertion qtoprest 
|- ( ph -> ( ( J qTop F ) |`t U ) = ( ( J |`t A ) qTop ( F |` A ) ) )

Proof

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