Proof of Theorem wrdlen2i
Step | Hyp | Ref
| Expression |
1 | | c0ex 10980 |
. . . . . . 7
⊢ 0 ∈
V |
2 | | 1ex 10982 |
. . . . . . 7
⊢ 1 ∈
V |
3 | 1, 2 | pm3.2i 471 |
. . . . . 6
⊢ (0 ∈
V ∧ 1 ∈ V) |
4 | | simpl 483 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉)) |
5 | | 0ne1 12055 |
. . . . . . 7
⊢ 0 ≠
1 |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → 0 ≠ 1) |
7 | | fprg 7024 |
. . . . . 6
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ (𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 0 ≠ 1) → {〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇}) |
8 | 3, 4, 6, 7 | mp3an2i 1465 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → {〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇}) |
9 | | fzo0to2pr 13483 |
. . . . . . . . . . . . . 14
⊢ (0..^2) =
{0, 1} |
10 | 9 | eqcomi 2749 |
. . . . . . . . . . . . 13
⊢ {0, 1} =
(0..^2) |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → {0, 1} = (0..^2)) |
12 | 11 | feq2d 6584 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇} ↔ {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶{𝑆, 𝑇})) |
13 | 12 | biimpa 477 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ {〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇}) → {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶{𝑆, 𝑇}) |
14 | | prssi 4760 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → {𝑆, 𝑇} ⊆ 𝑉) |
15 | 14 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ {〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇}) → {𝑆, 𝑇} ⊆ 𝑉) |
16 | 13, 15 | fssd 6616 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ {〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇}) → {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶𝑉) |
17 | 16 | ex 413 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇} → {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶𝑉)) |
18 | 17 | adantr 481 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → ({〈0, 𝑆〉, 〈1, 𝑇〉}:{0, 1}⟶{𝑆, 𝑇} → {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶𝑉)) |
19 | 18 | impcom 408 |
. . . . . 6
⊢
(({〈0, 𝑆〉,
〈1, 𝑇〉}:{0,
1}⟶{𝑆, 𝑇} ∧ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉})) → {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶𝑉) |
20 | | feq1 6579 |
. . . . . . . 8
⊢ (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → (𝑊:(0..^2)⟶𝑉 ↔ {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶𝑉)) |
21 | 20 | adantl 482 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → (𝑊:(0..^2)⟶𝑉 ↔ {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶𝑉)) |
22 | 21 | adantl 482 |
. . . . . 6
⊢
(({〈0, 𝑆〉,
〈1, 𝑇〉}:{0,
1}⟶{𝑆, 𝑇} ∧ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉})) → (𝑊:(0..^2)⟶𝑉 ↔ {〈0, 𝑆〉, 〈1, 𝑇〉}:(0..^2)⟶𝑉)) |
23 | 19, 22 | mpbird 256 |
. . . . 5
⊢
(({〈0, 𝑆〉,
〈1, 𝑇〉}:{0,
1}⟶{𝑆, 𝑇} ∧ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉})) → 𝑊:(0..^2)⟶𝑉) |
24 | 8, 23 | mpancom 685 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → 𝑊:(0..^2)⟶𝑉) |
25 | | iswrdi 14232 |
. . . 4
⊢ (𝑊:(0..^2)⟶𝑉 → 𝑊 ∈ Word 𝑉) |
26 | 24, 25 | syl 17 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → 𝑊 ∈ Word 𝑉) |
27 | | fveq2 6771 |
. . . 4
⊢ (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → (♯‘𝑊) = (♯‘{〈0,
𝑆〉, 〈1, 𝑇〉})) |
28 | 5 | neii 2947 |
. . . . . . 7
⊢ ¬ 0
= 1 |
29 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → 𝑆 ∈ 𝑉) |
30 | | opth1g 5397 |
. . . . . . . 8
⊢ ((0
∈ V ∧ 𝑆 ∈
𝑉) → (〈0, 𝑆〉 = 〈1, 𝑇〉 → 0 =
1)) |
31 | 1, 29, 30 | sylancr 587 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (〈0, 𝑆〉 = 〈1, 𝑇〉 → 0 = 1)) |
32 | 28, 31 | mtoi 198 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ¬ 〈0, 𝑆〉 = 〈1, 𝑇〉) |
33 | 32 | neqned 2952 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → 〈0, 𝑆〉 ≠ 〈1, 𝑇〉) |
34 | | opex 5383 |
. . . . . . 7
⊢ 〈0,
𝑆〉 ∈
V |
35 | | opex 5383 |
. . . . . . 7
⊢ 〈1,
𝑇〉 ∈
V |
36 | 34, 35 | pm3.2i 471 |
. . . . . 6
⊢ (〈0,
𝑆〉 ∈ V ∧
〈1, 𝑇〉 ∈
V) |
37 | | hashprg 14121 |
. . . . . 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 2802 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → (♯‘𝑊) = 2) |
41 | 5 | a1i 11 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → 0 ≠ 1) |
42 | | fvpr1g 7059 |
. . . . . . 7
⊢ ((0
∈ V ∧ 𝑆 ∈
𝑉 ∧ 0 ≠ 1) →
({〈0, 𝑆〉,
〈1, 𝑇〉}‘0)
= 𝑆) |
43 | 1, 29, 41, 42 | mp3an2i 1465 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({〈0, 𝑆〉, 〈1, 𝑇〉}‘0) = 𝑆) |
44 | | simpr 485 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → 𝑇 ∈ 𝑉) |
45 | | fvpr2g 7060 |
. . . . . . 7
⊢ ((1
∈ V ∧ 𝑇 ∈
𝑉 ∧ 0 ≠ 1) →
({〈0, 𝑆〉,
〈1, 𝑇〉}‘1)
= 𝑇) |
46 | 2, 44, 41, 45 | mp3an2i 1465 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → ({〈0, 𝑆〉, 〈1, 𝑇〉}‘1) = 𝑇) |
47 | 43, 46 | jca 512 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (({〈0, 𝑆〉, 〈1, 𝑇〉}‘0) = 𝑆 ∧ ({〈0, 𝑆〉, 〈1, 𝑇〉}‘1) = 𝑇)) |
48 | 47 | adantr 481 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → (({〈0, 𝑆〉, 〈1, 𝑇〉}‘0) = 𝑆 ∧ ({〈0, 𝑆〉, 〈1, 𝑇〉}‘1) = 𝑇)) |
49 | | fveq1 6770 |
. . . . . . 7
⊢ (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → (𝑊‘0) = ({〈0, 𝑆〉, 〈1, 𝑇〉}‘0)) |
50 | 49 | eqeq1d 2742 |
. . . . . 6
⊢ (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → ((𝑊‘0) = 𝑆 ↔ ({〈0, 𝑆〉, 〈1, 𝑇〉}‘0) = 𝑆)) |
51 | | fveq1 6770 |
. . . . . . 7
⊢ (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → (𝑊‘1) = ({〈0, 𝑆〉, 〈1, 𝑇〉}‘1)) |
52 | 51 | eqeq1d 2742 |
. . . . . 6
⊢ (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → ((𝑊‘1) = 𝑇 ↔ ({〈0, 𝑆〉, 〈1, 𝑇〉}‘1) = 𝑇)) |
53 | 50, 52 | anbi12d 631 |
. . . . 5
⊢ (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → (((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇) ↔ (({〈0, 𝑆〉, 〈1, 𝑇〉}‘0) = 𝑆 ∧ ({〈0, 𝑆〉, 〈1, 𝑇〉}‘1) = 𝑇))) |
54 | 53 | adantl 482 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → (((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇) ↔ (({〈0, 𝑆〉, 〈1, 𝑇〉}‘0) = 𝑆 ∧ ({〈0, 𝑆〉, 〈1, 𝑇〉}‘1) = 𝑇))) |
55 | 48, 54 | mpbird 256 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇)) |
56 | 26, 40, 55 | jca31 515 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) ∧ 𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉}) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇))) |
57 | 56 | ex 413 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇)))) |