pwssplit0

Description: Splitting for structure powers, part 0: restriction is a function. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwssplit1.y	$⊢ Y = W ↑_{𝑠} U$
	pwssplit1.z	$⊢ Z = W ↑_{𝑠} V$
	pwssplit1.b	$⊢ B = {Base}_{Y}$
	pwssplit1.c	$⊢ C = {Base}_{Z}$
	pwssplit1.f	$⊢ F = (x \in B ⟼ {x ↾}_{V})$
Assertion	pwssplit0	$⊢ (W \in T \land U \in X \land V \subseteq U) \to F : B ⟶ C$

Proof

Step	Hyp	Ref	Expression
1		pwssplit1.y	$⊢ Y = W ↑_{𝑠} U$
2		pwssplit1.z	$⊢ Z = W ↑_{𝑠} V$
3		pwssplit1.b	$⊢ B = {Base}_{Y}$
4		pwssplit1.c	$⊢ C = {Base}_{Z}$
5		pwssplit1.f	$⊢ F = (x \in B ⟼ {x ↾}_{V})$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7	1 6 3	pwselbasb	$⊢ (W \in T \land U \in X) \to (x \in B \leftrightarrow x : U ⟶ {Base}_{W})$
8	7	3adant3	$⊢ (W \in T \land U \in X \land V \subseteq U) \to (x \in B \leftrightarrow x : U ⟶ {Base}_{W})$
9	8	biimpa	$⊢ ((W \in T \land U \in X \land V \subseteq U) \land x \in B) \to x : U ⟶ {Base}_{W}$
10		simpl3	$⊢ ((W \in T \land U \in X \land V \subseteq U) \land x \in B) \to V \subseteq U$
11	9 10	fssresd	$⊢ ((W \in T \land U \in X \land V \subseteq U) \land x \in B) \to ({x ↾}_{V}) : V ⟶ {Base}_{W}$
12		simp1	$⊢ (W \in T \land U \in X \land V \subseteq U) \to W \in T$
13		simp2	$⊢ (W \in T \land U \in X \land V \subseteq U) \to U \in X$
14		simp3	$⊢ (W \in T \land U \in X \land V \subseteq U) \to V \subseteq U$
15	13 14	ssexd	$⊢ (W \in T \land U \in X \land V \subseteq U) \to V \in V$
16	2 6 4	pwselbasb	$⊢ (W \in T \land V \in V) \to ({x ↾}_{V} \in C \leftrightarrow ({x ↾}_{V}) : V ⟶ {Base}_{W})$
17	12 15 16	syl2anc	$⊢ (W \in T \land U \in X \land V \subseteq U) \to ({x ↾}_{V} \in C \leftrightarrow ({x ↾}_{V}) : V ⟶ {Base}_{W})$
18	17	adantr	$⊢ ((W \in T \land U \in X \land V \subseteq U) \land x \in B) \to ({x ↾}_{V} \in C \leftrightarrow ({x ↾}_{V}) : V ⟶ {Base}_{W})$
19	11 18	mpbird	$⊢ ((W \in T \land U \in X \land V \subseteq U) \land x \in B) \to {x ↾}_{V} \in C$
20	19 5	fmptd	$⊢ (W \in T \land U \in X \land V \subseteq U) \to F : B ⟶ C$

Metamath Proof Explorer

Theorem pwssplit0

Proof