Proof of Theorem wlkntrllem2
Step | Hyp | Ref
| Expression |
1 | | wlkntrl.f |
. . . . . . 7
⊢ 𝐹 = {〈0, 0〉, 〈1,
0〉} |
2 | 1 | fveq1i 6104 |
. . . . . 6
⊢ (𝐹‘0) = ({〈0, 0〉,
〈1, 0〉}‘0) |
3 | | 0ne1 10965 |
. . . . . . 7
⊢ 0 ≠
1 |
4 | | c0ex 9913 |
. . . . . . . 8
⊢ 0 ∈
V |
5 | 4, 4 | fvpr1 6361 |
. . . . . . 7
⊢ (0 ≠ 1
→ ({〈0, 0〉, 〈1, 0〉}‘0) = 0) |
6 | 3, 5 | ax-mp 5 |
. . . . . 6
⊢
({〈0, 0〉, 〈1, 0〉}‘0) = 0 |
7 | 2, 6 | eqtri 2632 |
. . . . 5
⊢ (𝐹‘0) = 0 |
8 | 7 | fveq2i 6106 |
. . . 4
⊢ (𝐸‘(𝐹‘0)) = (𝐸‘0) |
9 | | wlkntrl.e |
. . . . . 6
⊢ 𝐸 = {〈0, {𝑥, 𝑦}〉} |
10 | 9 | fveq1i 6104 |
. . . . 5
⊢ (𝐸‘0) = ({〈0, {𝑥, 𝑦}〉}‘0) |
11 | | prex 4836 |
. . . . . 6
⊢ {𝑥, 𝑦} ∈ V |
12 | 4, 11 | fvsn 6351 |
. . . . 5
⊢
({〈0, {𝑥, 𝑦}〉}‘0) = {𝑥, 𝑦} |
13 | 10, 12 | eqtri 2632 |
. . . 4
⊢ (𝐸‘0) = {𝑥, 𝑦} |
14 | | wlkntrl.p |
. . . . . . 7
⊢ 𝑃 = {〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉} |
15 | 14 | fveq1i 6104 |
. . . . . 6
⊢ (𝑃‘0) = ({〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉}‘0) |
16 | | 0ne2 11116 |
. . . . . . 7
⊢ 0 ≠
2 |
17 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
18 | 4, 17 | fvtp1 6365 |
. . . . . . 7
⊢ ((0 ≠
1 ∧ 0 ≠ 2) → ({〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉}‘0) = 𝑥) |
19 | 3, 16, 18 | mp2an 704 |
. . . . . 6
⊢
({〈0, 𝑥〉,
〈1, 𝑦〉, 〈2,
𝑥〉}‘0) = 𝑥 |
20 | 15, 19 | eqtr2i 2633 |
. . . . 5
⊢ 𝑥 = (𝑃‘0) |
21 | 14 | fveq1i 6104 |
. . . . . 6
⊢ (𝑃‘1) = ({〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉}‘1) |
22 | | 1ne2 11117 |
. . . . . . 7
⊢ 1 ≠
2 |
23 | | 1ex 9914 |
. . . . . . . 8
⊢ 1 ∈
V |
24 | | vex 3176 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
25 | 23, 24 | fvtp2 6366 |
. . . . . . 7
⊢ ((0 ≠
1 ∧ 1 ≠ 2) → ({〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉}‘1) = 𝑦) |
26 | 3, 22, 25 | mp2an 704 |
. . . . . 6
⊢
({〈0, 𝑥〉,
〈1, 𝑦〉, 〈2,
𝑥〉}‘1) = 𝑦 |
27 | 21, 26 | eqtr2i 2633 |
. . . . 5
⊢ 𝑦 = (𝑃‘1) |
28 | 20, 27 | preq12i 4217 |
. . . 4
⊢ {𝑥, 𝑦} = {(𝑃‘0), (𝑃‘1)} |
29 | 8, 13, 28 | 3eqtri 2636 |
. . 3
⊢ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} |
30 | 1 | fveq1i 6104 |
. . . . . 6
⊢ (𝐹‘1) = ({〈0, 0〉,
〈1, 0〉}‘1) |
31 | 23, 4 | fvpr2 6362 |
. . . . . . 7
⊢ (0 ≠ 1
→ ({〈0, 0〉, 〈1, 0〉}‘1) = 0) |
32 | 3, 31 | ax-mp 5 |
. . . . . 6
⊢
({〈0, 0〉, 〈1, 0〉}‘1) = 0 |
33 | 30, 32 | eqtri 2632 |
. . . . 5
⊢ (𝐹‘1) = 0 |
34 | 33 | fveq2i 6106 |
. . . 4
⊢ (𝐸‘(𝐹‘1)) = (𝐸‘0) |
35 | | prcom 4211 |
. . . . 5
⊢ {𝑥, 𝑦} = {𝑦, 𝑥} |
36 | 14 | fveq1i 6104 |
. . . . . . 7
⊢ (𝑃‘2) = ({〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉}‘2) |
37 | | 2ex 10969 |
. . . . . . . . 9
⊢ 2 ∈
V |
38 | 37, 17 | fvtp3 6367 |
. . . . . . . 8
⊢ ((0 ≠
2 ∧ 1 ≠ 2) → ({〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉}‘2) = 𝑥) |
39 | 16, 22, 38 | mp2an 704 |
. . . . . . 7
⊢
({〈0, 𝑥〉,
〈1, 𝑦〉, 〈2,
𝑥〉}‘2) = 𝑥 |
40 | 36, 39 | eqtr2i 2633 |
. . . . . 6
⊢ 𝑥 = (𝑃‘2) |
41 | 27, 40 | preq12i 4217 |
. . . . 5
⊢ {𝑦, 𝑥} = {(𝑃‘1), (𝑃‘2)} |
42 | 35, 41 | eqtri 2632 |
. . . 4
⊢ {𝑥, 𝑦} = {(𝑃‘1), (𝑃‘2)} |
43 | 34, 13, 42 | 3eqtri 2636 |
. . 3
⊢ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} |
44 | | 0p1e1 11009 |
. . . . . 6
⊢ (0 + 1) =
1 |
45 | 44 | preq2i 4216 |
. . . . 5
⊢ {0, (0 +
1)} = {0, 1} |
46 | 45 | raleqi 3119 |
. . . 4
⊢
(∀𝑘 ∈
{0, (0 + 1)} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
47 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) |
48 | 47 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 0 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘0))) |
49 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
50 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
51 | 50, 44 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
52 | 51 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
53 | 49, 52 | preq12d 4220 |
. . . . . 6
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
54 | 48, 53 | eqeq12d 2625 |
. . . . 5
⊢ (𝑘 = 0 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
55 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
56 | 55 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 1 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘1))) |
57 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
58 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
59 | | 1p1e2 11011 |
. . . . . . . . 9
⊢ (1 + 1) =
2 |
60 | 58, 59 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
61 | 60 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
62 | 57, 61 | preq12d 4220 |
. . . . . 6
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
63 | 56, 62 | eqeq12d 2625 |
. . . . 5
⊢ (𝑘 = 1 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
64 | 4, 23, 54, 63 | ralpr 4185 |
. . . 4
⊢
(∀𝑘 ∈
{0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
65 | 46, 64 | bitri 263 |
. . 3
⊢
(∀𝑘 ∈
{0, (0 + 1)} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
66 | 29, 43, 65 | mpbir2an 957 |
. 2
⊢
∀𝑘 ∈ {0,
(0 + 1)} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} |
67 | | 0z 11265 |
. . . . . . 7
⊢ 0 ∈
ℤ |
68 | 67, 67 | pm3.2i 470 |
. . . . . 6
⊢ (0 ∈
ℤ ∧ 0 ∈ ℤ) |
69 | 68, 1 | 2trllemA 26080 |
. . . . 5
⊢
(#‘𝐹) =
2 |
70 | 69 | oveq2i 6560 |
. . . 4
⊢
(0..^(#‘𝐹)) =
(0..^2) |
71 | | 2z 11286 |
. . . . 5
⊢ 2 ∈
ℤ |
72 | | fzoval 12340 |
. . . . 5
⊢ (2 ∈
ℤ → (0..^2) = (0...(2 − 1))) |
73 | 71, 72 | ax-mp 5 |
. . . 4
⊢ (0..^2) =
(0...(2 − 1)) |
74 | | 2m1e1 11012 |
. . . . . 6
⊢ (2
− 1) = 1 |
75 | 74 | oveq2i 6560 |
. . . . 5
⊢ (0...(2
− 1)) = (0...1) |
76 | | 1e0p1 11428 |
. . . . . 6
⊢ 1 = (0 +
1) |
77 | 76 | oveq2i 6560 |
. . . . 5
⊢ (0...1) =
(0...(0 + 1)) |
78 | | fzpr 12266 |
. . . . . 6
⊢ (0 ∈
ℤ → (0...(0 + 1)) = {0, (0 + 1)}) |
79 | 67, 78 | ax-mp 5 |
. . . . 5
⊢ (0...(0 +
1)) = {0, (0 + 1)} |
80 | 75, 77, 79 | 3eqtri 2636 |
. . . 4
⊢ (0...(2
− 1)) = {0, (0 + 1)} |
81 | 70, 73, 80 | 3eqtri 2636 |
. . 3
⊢
(0..^(#‘𝐹)) =
{0, (0 + 1)} |
82 | 81 | raleqi 3119 |
. 2
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, (0 + 1)} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
83 | 66, 82 | mpbir 220 |
1
⊢
∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} |