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