Step |
Hyp |
Ref |
Expression |
1 |
|
estrcbasbas.c |
⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 ) |
2 |
|
estrcbasbas.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
estrcbasbas.u |
⊢ ( 𝜑 → 𝑈 ∈ WUni ) |
4 |
1 3
|
estrcbas |
⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) ) |
5 |
2 4
|
eqtr4id |
⊢ ( 𝜑 → 𝐵 = 𝑈 ) |
6 |
5
|
eleq2d |
⊢ ( 𝜑 → ( 𝐸 ∈ 𝐵 ↔ 𝐸 ∈ 𝑈 ) ) |
7 |
|
baseid |
⊢ Base = Slot ( Base ‘ ndx ) |
8 |
|
simpl |
⊢ ( ( 𝑈 ∈ WUni ∧ 𝐸 ∈ 𝑈 ) → 𝑈 ∈ WUni ) |
9 |
|
simpr |
⊢ ( ( 𝑈 ∈ WUni ∧ 𝐸 ∈ 𝑈 ) → 𝐸 ∈ 𝑈 ) |
10 |
7 8 9
|
wunstr |
⊢ ( ( 𝑈 ∈ WUni ∧ 𝐸 ∈ 𝑈 ) → ( Base ‘ 𝐸 ) ∈ 𝑈 ) |
11 |
10
|
ex |
⊢ ( 𝑈 ∈ WUni → ( 𝐸 ∈ 𝑈 → ( Base ‘ 𝐸 ) ∈ 𝑈 ) ) |
12 |
3 11
|
syl |
⊢ ( 𝜑 → ( 𝐸 ∈ 𝑈 → ( Base ‘ 𝐸 ) ∈ 𝑈 ) ) |
13 |
6 12
|
sylbid |
⊢ ( 𝜑 → ( 𝐸 ∈ 𝐵 → ( Base ‘ 𝐸 ) ∈ 𝑈 ) ) |
14 |
13
|
imp |
⊢ ( ( 𝜑 ∧ 𝐸 ∈ 𝐵 ) → ( Base ‘ 𝐸 ) ∈ 𝑈 ) |