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	$⊢ φ \to J \in TopOn (X)$
	qtoprest.3	$⊢ φ \to F : X \underset{onto}{⟶} Y$
	qtoprest.4	$⊢ φ \to U \subseteq Y$
	qtoprest.5	$⊢ φ \to A = F^{-1} [U]$
	qtoprest.6	$⊢ φ \to (A \in J \lor A \in Clsd (J))$
Assertion	qtoprest	$⊢ φ \to (J qTop F) ↾_{𝑡} U = (J ↾_{𝑡} A) qTop ({F ↾}_{A})$

Proof

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

Metamath Proof Explorer

Theorem qtoprest

Proof