Metamath Proof Explorer

Theorem 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 ∈ B ⟼ x ↾ V
Assertion pwssplit0 ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → 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 ∈ B ⟼ x ↾ V
6 eqid ⊢ Base W = Base W
7 1 6 3 pwselbasb ⊢ W ∈ T ∧ U ∈ X → x ∈ B ↔ x : U ⟶ Base W
8 7 3adant3 ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → x ∈ B ↔ x : U ⟶ Base W
9 8 biimpa ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U ∧ x ∈ B → x : U ⟶ Base W
10 simpl3 ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U ∧ x ∈ B → V ⊆ U
11 9 10 fssresd ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U ∧ x ∈ B → x ↾ V : V ⟶ Base W
12 simp1 ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → W ∈ T
13 simp2 ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → U ∈ X
14 simp3 ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → V ⊆ U
15 13 14 ssexd ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → V ∈ V
16 2 6 4 pwselbasb ⊢ W ∈ T ∧ V ∈ V → x ↾ V ∈ C ↔ x ↾ V : V ⟶ Base W
17 12 15 16 syl2anc ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → x ↾ V ∈ C ↔ x ↾ V : V ⟶ Base W
18 17 adantr ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U ∧ x ∈ B → x ↾ V ∈ C ↔ x ↾ V : V ⟶ Base W
19 11 18 mpbird ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U ∧ x ∈ B → x ↾ V ∈ C
20 19 5 fmptd ⊢ W ∈ T ∧ U ∈ X ∧ V ⊆ U → F : B ⟶ C