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 Top$
	resthauslem.2	$⊢ (J \in A \land ({I ↾}_{(S \cap ⋃ J)}) : S \cap ⋃ J \underset{1-1}{⟶} S \cap ⋃ J \land {I ↾}_{(S \cap ⋃ J)} \in ((J ↾_{𝑡} S) Cn J)) \to J ↾_{𝑡} S \in A$
Assertion	resthauslem	$⊢ (J \in A \land S \in V) \to J ↾_{𝑡} S \in A$

Proof

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

Metamath Proof Explorer

Theorem resthauslem

Proof