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 ⊢ 𝑌 = ( 𝑊 ↑s 𝑈 )
pwssplit1.z ⊢ 𝑍 = ( 𝑊 ↑s 𝑉 )
pwssplit1.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwssplit1.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
pwssplit1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
Assertion pwssplit0 ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 : 𝐵 ⟶ 𝐶 )

Proof

Step Hyp Ref Expression
1 pwssplit1.y ⊢ 𝑌 = ( 𝑊 ↑s 𝑈 )
2 pwssplit1.z ⊢ 𝑍 = ( 𝑊 ↑s 𝑉 )
3 pwssplit1.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
4 pwssplit1.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
5 pwssplit1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
6 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 1 6 3 pwselbasb ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 : 𝑈 ⟶ ( Base ‘ 𝑊 ) ) )
8 7 3adant3 ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 : 𝑈 ⟶ ( Base ‘ 𝑊 ) ) )
9 8 biimpa ⊢ ( ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 : 𝑈 ⟶ ( Base ‘ 𝑊 ) )
10 simpl3 ⊢ ( ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑉 ⊆ 𝑈 )
11 9 10 fssresd ⊢ ( ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑊 ) )
12 simp1 ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑊 ∈ 𝑇 )
13 simp2 ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑈 ∈ 𝑋 )
14 simp3 ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ⊆ 𝑈 )
15 13 14 ssexd ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ∈ V )
16 2 6 4 pwselbasb ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑉 ∈ V ) → ( ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 ↔ ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑊 ) ) )
17 12 15 16 syl2anc ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 ↔ ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑊 ) ) )
18 17 adantr ⊢ ( ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 ↔ ( 𝑥 ↾ 𝑉 ) : 𝑉 ⟶ ( Base ‘ 𝑊 ) ) )
19 11 18 mpbird ⊢ ( ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ↾ 𝑉 ) ∈ 𝐶 )
20 19 5 fmptd ⊢ ( ( 𝑊 ∈ 𝑇 ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 : 𝐵 ⟶ 𝐶 )