Step | Hyp | Ref
| Expression |
1 | | c0ex 11156 |
. . . . . . 7
⊢ 0 ∈
V |
2 | | 1ex 11158 |
. . . . . . 7
⊢ 1 ∈
V |
3 | 1, 2 | pm3.2i 472 |
. . . . . 6
⊢ (0 ∈
V ∧ 1 ∈ V) |
4 | | simpl 484 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉)) |
5 | | 0ne1 12231 |
. . . . . . 7
⊢ 0 ≠
1 |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → 0 ≠ 1) |
7 | | fprg 7106 |
. . . . . 6
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 0 ≠ 1) → {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇}) |
8 | 3, 4, 6, 7 | mp3an2i 1467 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇}) |
9 | | fzo0to2pr 13664 |
. . . . . . . . . . . . . 14
⊢ (0..^2) =
{0, 1} |
10 | 9 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ {0, 1} =
(0..^2) |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → {0, 1} = (0..^2)) |
12 | 11 | feq2d 6659 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇} ↔ {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶{𝑆, 𝑇})) |
13 | 12 | biimpa 478 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇}) → {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶{𝑆, 𝑇}) |
14 | | prssi 4786 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → {𝑆, 𝑇} ⊆ 𝑉) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇}) → {𝑆, 𝑇} ⊆ 𝑉) |
16 | 13, 15 | fssd 6691 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇}) → {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶𝑉) |
17 | 16 | ex 414 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇} → {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶𝑉)) |
18 | 17 | adantr 482 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:{0, 1}⟶{𝑆, 𝑇} → {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶𝑉)) |
19 | 18 | impcom 409 |
. . . . . 6
⊢
(({⟨0, 𝑆⟩,
⟨1, 𝑇⟩}:{0,
1}⟶{𝑆, 𝑇} ∧ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩})) → {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶𝑉) |
20 | | feq1 6654 |
. . . . . . . 8
⊢ (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → (𝑊:(0..^2)⟶𝑉 ↔ {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶𝑉)) |
21 | 20 | adantl 483 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → (𝑊:(0..^2)⟶𝑉 ↔ {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶𝑉)) |
22 | 21 | adantl 483 |
. . . . . 6
⊢
(({⟨0, 𝑆⟩,
⟨1, 𝑇⟩}:{0,
1}⟶{𝑆, 𝑇} ∧ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩})) → (𝑊:(0..^2)⟶𝑉 ↔ {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}:(0..^2)⟶𝑉)) |
23 | 19, 22 | mpbird 257 |
. . . . 5
⊢
(({⟨0, 𝑆⟩,
⟨1, 𝑇⟩}:{0,
1}⟶{𝑆, 𝑇} ∧ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩})) → 𝑊:(0..^2)⟶𝑉) |
24 | 8, 23 | mpancom 687 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → 𝑊:(0..^2)⟶𝑉) |
25 | | iswrdi 14413 |
. . . 4
⊢ (𝑊:(0..^2)⟶𝑉 → 𝑊 ∈ Word 𝑉) |
26 | 24, 25 | syl 17 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → 𝑊 ∈ Word 𝑉) |
27 | | fveq2 6847 |
. . . 4
⊢ (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → (♯‘𝑊) = (♯‘{⟨0,
𝑆⟩, ⟨1, 𝑇⟩})) |
28 | 5 | neii 2946 |
. . . . . . 7
⊢ ¬ 0
= 1 |
29 | | simpl 484 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → 𝑆 ∈ 𝑉) |
30 | | opth1g 5440 |
. . . . . . . 8
⊢ ((0
∈ V ∧ 𝑆 ∈
𝑉) → (⟨0, 𝑆⟩ = ⟨1, 𝑇⟩ → 0 =
1)) |
31 | 1, 29, 30 | sylancr 588 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (⟨0, 𝑆⟩ = ⟨1, 𝑇⟩ → 0 = 1)) |
32 | 28, 31 | mtoi 198 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ¬ ⟨0, 𝑆⟩ = ⟨1, 𝑇⟩) |
33 | 32 | neqned 2951 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ⟨0, 𝑆⟩ ≠ ⟨1, 𝑇⟩) |
34 | | opex 5426 |
. . . . . . 7
⊢ ⟨0,
𝑆⟩ ∈
V |
35 | | opex 5426 |
. . . . . . 7
⊢ ⟨1,
𝑇⟩ ∈
V |
36 | 34, 35 | pm3.2i 472 |
. . . . . 6
⊢ (⟨0,
𝑆⟩ ∈ V ∧
⟨1, 𝑇⟩ ∈
V) |
37 | | hashprg 14302 |
. . . . . 6
⊢
((⟨0, 𝑆⟩
∈ V ∧ ⟨1, 𝑇⟩ ∈ V) → (⟨0, 𝑆⟩ ≠ ⟨1, 𝑇⟩ ↔
(♯‘{⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) = 2)) |
38 | 36, 37 | mp1i 13 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (⟨0, 𝑆⟩ ≠ ⟨1, 𝑇⟩ ↔ (♯‘{⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) = 2)) |
39 | 33, 38 | mpbid 231 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (♯‘{⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) = 2) |
40 | 27, 39 | sylan9eqr 2799 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → (♯‘𝑊) = 2) |
41 | 5 | a1i 11 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → 0 ≠ 1) |
42 | | fvpr1g 7141 |
. . . . . . 7
⊢ ((0
∈ V ∧ 𝑆 ∈
𝑉 ∧ 0 ≠ 1) →
({⟨0, 𝑆⟩,
⟨1, 𝑇⟩}‘0)
= 𝑆) |
43 | 1, 29, 41, 42 | mp3an2i 1467 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘0) = 𝑆) |
44 | | simpr 486 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → 𝑇 ∈ 𝑉) |
45 | | fvpr2g 7142 |
. . . . . . 7
⊢ ((1
∈ V ∧ 𝑇 ∈
𝑉 ∧ 0 ≠ 1) →
({⟨0, 𝑆⟩,
⟨1, 𝑇⟩}‘1)
= 𝑇) |
46 | 2, 44, 41, 45 | mp3an2i 1467 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘1) = 𝑇) |
47 | 43, 46 | jca 513 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘0) = 𝑆 ∧ ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘1) = 𝑇)) |
48 | 47 | adantr 482 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → (({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘0) = 𝑆 ∧ ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘1) = 𝑇)) |
49 | | fveq1 6846 |
. . . . . . 7
⊢ (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → (𝑊‘0) = ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘0)) |
50 | 49 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → ((𝑊‘0) = 𝑆 ↔ ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘0) = 𝑆)) |
51 | | fveq1 6846 |
. . . . . . 7
⊢ (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → (𝑊‘1) = ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘1)) |
52 | 51 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → ((𝑊‘1) = 𝑇 ↔ ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘1) = 𝑇)) |
53 | 50, 52 | anbi12d 632 |
. . . . 5
⊢ (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → (((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇) ↔ (({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘0) = 𝑆 ∧ ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘1) = 𝑇))) |
54 | 53 | adantl 483 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → (((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇) ↔ (({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘0) = 𝑆 ∧ ({⟨0, 𝑆⟩, ⟨1, 𝑇⟩}‘1) = 𝑇))) |
55 | 48, 54 | mpbird 257 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇)) |
56 | 26, 40, 55 | jca31 516 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩}) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇))) |
57 | 56 | ex 414 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {⟨0, 𝑆⟩, ⟨1, 𝑇⟩} → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇)))) |