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 ( ( 𝑊𝑇𝑈𝑋𝑉𝑈 ) → 𝐹 : 𝐵𝐶 )