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

Metamath Proof Explorer

Theorem qtoprest

Proof