Theorem resthauslem

Description: Lemma for resthaus and similar theorems. If the topological property A is preserved under injective preimages, then property A passes to subspaces. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypotheses	resthauslem.1	$$⊢J\in A\to J\in \mathrm{Top}$$
	resthauslem.2	$$⊢\left(J\in A\wedge \left({\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\right):S\cap \bigcup J\underset{1-1}{⟶}S\cap \bigcup J\wedge {\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\in \left(\left(J{\upharpoonright }_{𝑡}S\right)\mathrm{Cn}J\right)\right)\to J{\upharpoonright }_{𝑡}S\in A$$
Assertion	resthauslem	$$⊢\left(J\in A\wedge S\in V\right)\to J{\upharpoonright }_{𝑡}S\in A$$

Proof

Step	Hyp	Ref	Expression
1		resthauslem.1	$$⊢J\in A\to J\in \mathrm{Top}$$
2		resthauslem.2	$$⊢\left(J\in A\wedge \left({\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\right):S\cap \bigcup J\underset{1-1}{⟶}S\cap \bigcup J\wedge {\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\in \left(\left(J{\upharpoonright }_{𝑡}S\right)\mathrm{Cn}J\right)\right)\to J{\upharpoonright }_{𝑡}S\in A$$
3		simpl	$$⊢\left(J\in A\wedge S\in V\right)\to J\in A$$
4		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\right):S\cap \bigcup J\underset{1-1\; onto}{⟶}S\cap \bigcup J$$
5		f1of1	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\right):S\cap \bigcup J\underset{1-1\; onto}{⟶}S\cap \bigcup J\to \left({\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\right):S\cap \bigcup J\underset{1-1}{⟶}S\cap \bigcup J$$
6	4 5	mp1i	$$⊢\left(J\in A\wedge S\in V\right)\to \left({\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\right):S\cap \bigcup J\underset{1-1}{⟶}S\cap \bigcup J$$
7		inss2	$$⊢S\cap \bigcup J\subseteq \bigcup J$$
8		resabs1	$$⊢S\cap \bigcup J\subseteq \bigcup J\to {\left({\mathrm{I}\upharpoonright }_{\bigcup J}\right)\upharpoonright }_{\left(S\cap \bigcup J\right)}={\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}$$
9	7 8	ax-mp	$$⊢{\left({\mathrm{I}\upharpoonright }_{\bigcup J}\right)\upharpoonright }_{\left(S\cap \bigcup J\right)}={\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}$$
10	1	adantr	$$⊢\left(J\in A\wedge S\in V\right)\to J\in \mathrm{Top}$$
11		toptopon2	$$⊢J\in \mathrm{Top}\leftrightarrow J\in \mathrm{TopOn}\left(\bigcup J\right)$$
12	10 11	sylib	$$⊢\left(J\in A\wedge S\in V\right)\to J\in \mathrm{TopOn}\left(\bigcup J\right)$$
13		idcn	$$⊢J\in \mathrm{TopOn}\left(\bigcup J\right)\to {\mathrm{I}\upharpoonright }_{\bigcup J}\in \left(J\mathrm{Cn}J\right)$$
14	12 13	syl	$$⊢\left(J\in A\wedge S\in V\right)\to {\mathrm{I}\upharpoonright }_{\bigcup J}\in \left(J\mathrm{Cn}J\right)$$
15		eqid	$$⊢\bigcup J=\bigcup J$$
16	15	cnrest	$$⊢\left({\mathrm{I}\upharpoonright }_{\bigcup J}\in \left(J\mathrm{Cn}J\right)\wedge S\cap \bigcup J\subseteq \bigcup J\right)\to {\left({\mathrm{I}\upharpoonright }_{\bigcup J}\right)\upharpoonright }_{\left(S\cap \bigcup J\right)}\in \left(\left(J{\upharpoonright }_{𝑡}\left(S\cap \bigcup J\right)\right)\mathrm{Cn}J\right)$$
17	14 7 16	sylancl	$$⊢\left(J\in A\wedge S\in V\right)\to {\left({\mathrm{I}\upharpoonright }_{\bigcup J}\right)\upharpoonright }_{\left(S\cap \bigcup J\right)}\in \left(\left(J{\upharpoonright }_{𝑡}\left(S\cap \bigcup J\right)\right)\mathrm{Cn}J\right)$$
18	9 17	eqeltrrid	$$⊢\left(J\in A\wedge S\in V\right)\to {\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\in \left(\left(J{\upharpoonright }_{𝑡}\left(S\cap \bigcup J\right)\right)\mathrm{Cn}J\right)$$
19	15	restin	$$⊢\left(J\in A\wedge S\in V\right)\to J{\upharpoonright }_{𝑡}S=J{\upharpoonright }_{𝑡}\left(S\cap \bigcup J\right)$$
20	19	oveq1d	$$⊢\left(J\in A\wedge S\in V\right)\to \left(J{\upharpoonright }_{𝑡}S\right)\mathrm{Cn}J=\left(J{\upharpoonright }_{𝑡}\left(S\cap \bigcup J\right)\right)\mathrm{Cn}J$$
21	18 20	eleqtrrd	$$⊢\left(J\in A\wedge S\in V\right)\to {\mathrm{I}\upharpoonright }_{\left(S\cap \bigcup J\right)}\in \left(\left(J{\upharpoonright }_{𝑡}S\right)\mathrm{Cn}J\right)$$
22	3 6 21 2	syl3anc	$$⊢\left(J\in A\wedge S\in V\right)\to J{\upharpoonright }_{𝑡}S\in A$$