Proof of Theorem 2strbasg
Step | Hyp | Ref
| Expression |
1 | | baseslid 12465 |
. 2
⊢ (Base =
Slot (Base‘ndx) ∧ (Base‘ndx) ∈ ℕ) |
2 | | 2str.g |
. . 3
⊢ 𝐺 = {〈(Base‘ndx),
𝐵〉, 〈(𝐸‘ndx), + 〉} |
3 | | basendxnn 12464 |
. . . . . 6
⊢
(Base‘ndx) ∈ ℕ |
4 | 3 | a1i 9 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → (Base‘ndx) ∈
ℕ) |
5 | | simpl 108 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 ∈ 𝑉) |
6 | | opexg 4211 |
. . . . 5
⊢
(((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ 𝑉) → 〈(Base‘ndx), 𝐵〉 ∈
V) |
7 | 4, 5, 6 | syl2anc 409 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 〈(Base‘ndx), 𝐵〉 ∈
V) |
8 | | 2str.e |
. . . . . . . 8
⊢ 𝐸 = Slot 𝑁 |
9 | | 2str.n |
. . . . . . . 8
⊢ 𝑁 ∈ ℕ |
10 | 8, 9 | ndxarg 12432 |
. . . . . . 7
⊢ (𝐸‘ndx) = 𝑁 |
11 | 10, 9 | eqeltri 2243 |
. . . . . 6
⊢ (𝐸‘ndx) ∈
ℕ |
12 | 11 | a1i 9 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → (𝐸‘ndx) ∈ ℕ) |
13 | | simpr 109 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + ∈ 𝑊) |
14 | | opexg 4211 |
. . . . 5
⊢ (((𝐸‘ndx) ∈ ℕ ∧
+ ∈
𝑊) → 〈(𝐸‘ndx), + 〉 ∈
V) |
15 | 12, 13, 14 | syl2anc 409 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 〈(𝐸‘ndx), + 〉 ∈
V) |
16 | | prexg 4194 |
. . . 4
⊢
((〈(Base‘ndx), 𝐵〉 ∈ V ∧ 〈(𝐸‘ndx), + 〉 ∈ V) →
{〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} ∈
V) |
17 | 7, 15, 16 | syl2anc 409 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} ∈
V) |
18 | 2, 17 | eqeltrid 2257 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 ∈ V) |
19 | 3 | nnrei 8880 |
. . . . . 6
⊢
(Base‘ndx) ∈ ℝ |
20 | | 2str.l |
. . . . . . 7
⊢ 1 <
𝑁 |
21 | | basendx 12463 |
. . . . . . 7
⊢
(Base‘ndx) = 1 |
22 | 20, 21, 10 | 3brtr4i 4017 |
. . . . . 6
⊢
(Base‘ndx) < (𝐸‘ndx) |
23 | 19, 22 | ltneii 8009 |
. . . . 5
⊢
(Base‘ndx) ≠ (𝐸‘ndx) |
24 | 23 | a1i 9 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → (Base‘ndx) ≠ (𝐸‘ndx)) |
25 | | funprg 5246 |
. . . 4
⊢
((((Base‘ndx) ∈ ℕ ∧ (𝐸‘ndx) ∈ ℕ) ∧ (𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) ∧ (Base‘ndx) ≠ (𝐸‘ndx)) → Fun
{〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉}) |
26 | 4, 12, 5, 13, 24, 25 | syl221anc 1244 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → Fun {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉}) |
27 | 2 | funeqi 5217 |
. . 3
⊢ (Fun
𝐺 ↔ Fun
{〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉}) |
28 | 26, 27 | sylibr 133 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → Fun 𝐺) |
29 | | prid1g 3685 |
. . . 4
⊢
(〈(Base‘ndx), 𝐵〉 ∈ V →
〈(Base‘ndx), 𝐵〉 ∈ {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉}) |
30 | 7, 29 | syl 14 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 〈(Base‘ndx), 𝐵〉 ∈
{〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉}) |
31 | 30, 2 | eleqtrrdi 2264 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 〈(Base‘ndx), 𝐵〉 ∈ 𝐺) |
32 | 1, 18, 28, 31 | strslfvd 12450 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺)) |