Proof of Theorem wlkntrllem3
Step | Hyp | Ref
| Expression |
1 | | ax-1ne0 9884 |
. . 3
⊢ 1 ≠
0 |
2 | 1 | neii 2784 |
. 2
⊢ ¬ 1
= 0 |
3 | | 0ne1 10965 |
. . . . 5
⊢ 0 ≠
1 |
4 | | c0ex 9913 |
. . . . . 6
⊢ 0 ∈
V |
5 | | 1ex 9914 |
. . . . . 6
⊢ 1 ∈
V |
6 | 4, 5, 4, 4 | fpr 6326 |
. . . . 5
⊢ (0 ≠ 1
→ {〈0, 0〉, 〈1, 0〉}:{0, 1}⟶{0,
0}) |
7 | 3, 6 | ax-mp 5 |
. . . 4
⊢ {〈0,
0〉, 〈1, 0〉}:{0, 1}⟶{0, 0} |
8 | | wlkntrl.f |
. . . . . 6
⊢ 𝐹 = {〈0, 0〉, 〈1,
0〉} |
9 | 8 | eqcomi 2619 |
. . . . 5
⊢ {〈0,
0〉, 〈1, 0〉} = 𝐹 |
10 | 9 | feq1i 5949 |
. . . 4
⊢
({〈0, 0〉, 〈1, 0〉}:{0, 1}⟶{0, 0} ↔ 𝐹:{0, 1}⟶{0,
0}) |
11 | 7, 10 | mpbi 219 |
. . 3
⊢ 𝐹:{0, 1}⟶{0,
0} |
12 | | df-f1 5809 |
. . . 4
⊢ (𝐹:{0, 1}–1-1→{0, 0} ↔ (𝐹:{0, 1}⟶{0, 0} ∧ Fun ◡𝐹)) |
13 | | dff13 6416 |
. . . . 5
⊢ (𝐹:{0, 1}–1-1→{0, 0} ↔ (𝐹:{0, 1}⟶{0, 0} ∧ ∀𝑥 ∈ {0, 1}∀𝑦 ∈ {0, 1} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
14 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝐹‘𝑥) = (𝐹‘0)) |
15 | 14 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘0) = (𝐹‘𝑦))) |
16 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝑥 = 𝑦 ↔ 0 = 𝑦)) |
17 | 15, 16 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦))) |
18 | 17 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑥 = 0 → (∀𝑦 ∈ {0, 1} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {0, 1} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦))) |
19 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
20 | 19 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘1) = (𝐹‘𝑦))) |
21 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝑥 = 𝑦 ↔ 1 = 𝑦)) |
22 | 20, 21 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦))) |
23 | 22 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑥 = 1 → (∀𝑦 ∈ {0, 1} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {0, 1} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦))) |
24 | 4, 5, 18, 23 | ralpr 4185 |
. . . . . . 7
⊢
(∀𝑥 ∈
{0, 1}∀𝑦 ∈ {0,
1} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∀𝑦 ∈ {0, 1} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ∧ ∀𝑦 ∈ {0, 1} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦))) |
25 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → (𝐹‘𝑦) = (𝐹‘0)) |
26 | 25 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → ((𝐹‘0) = (𝐹‘𝑦) ↔ (𝐹‘0) = (𝐹‘0))) |
27 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (0 = 𝑦 ↔ 0 = 0)) |
28 | 26, 27 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ↔ ((𝐹‘0) = (𝐹‘0) → 0 = 0))) |
29 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (𝐹‘𝑦) = (𝐹‘1)) |
30 | 29 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → ((𝐹‘0) = (𝐹‘𝑦) ↔ (𝐹‘0) = (𝐹‘1))) |
31 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (0 = 𝑦 ↔ 0 = 1)) |
32 | 30, 31 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ↔ ((𝐹‘0) = (𝐹‘1) → 0 = 1))) |
33 | 4, 5, 28, 32 | ralpr 4185 |
. . . . . . . 8
⊢
(∀𝑦 ∈
{0, 1} ((𝐹‘0) =
(𝐹‘𝑦) → 0 = 𝑦) ↔ (((𝐹‘0) = (𝐹‘0) → 0 = 0) ∧ ((𝐹‘0) = (𝐹‘1) → 0 = 1))) |
34 | 25 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → ((𝐹‘1) = (𝐹‘𝑦) ↔ (𝐹‘1) = (𝐹‘0))) |
35 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (1 = 𝑦 ↔ 1 = 0)) |
36 | 34, 35 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = 0 → (((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ↔ ((𝐹‘1) = (𝐹‘0) → 1 = 0))) |
37 | 29 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → ((𝐹‘1) = (𝐹‘𝑦) ↔ (𝐹‘1) = (𝐹‘1))) |
38 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → (1 = 𝑦 ↔ 1 = 1)) |
39 | 37, 38 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = 1 → (((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ↔ ((𝐹‘1) = (𝐹‘1) → 1 = 1))) |
40 | 4, 5, 36, 39 | ralpr 4185 |
. . . . . . . 8
⊢
(∀𝑦 ∈
{0, 1} ((𝐹‘1) =
(𝐹‘𝑦) → 1 = 𝑦) ↔ (((𝐹‘1) = (𝐹‘0) → 1 = 0) ∧ ((𝐹‘1) = (𝐹‘1) → 1 = 1))) |
41 | 8 | fveq1i 6104 |
. . . . . . . . . . . . 13
⊢ (𝐹‘1) = ({〈0, 0〉,
〈1, 0〉}‘1) |
42 | 5, 4 | fvpr2 6362 |
. . . . . . . . . . . . . 14
⊢ (0 ≠ 1
→ ({〈0, 0〉, 〈1, 0〉}‘1) = 0) |
43 | 3, 42 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (¬ 1
= 0 → ({〈0, 0〉, 〈1, 0〉}‘1) = 0) |
44 | 41, 43 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (¬ 1
= 0 → (𝐹‘1) =
0) |
45 | 8 | fveq1i 6104 |
. . . . . . . . . . . . 13
⊢ (𝐹‘0) = ({〈0, 0〉,
〈1, 0〉}‘0) |
46 | 4, 4 | fvpr1 6361 |
. . . . . . . . . . . . . 14
⊢ (0 ≠ 1
→ ({〈0, 0〉, 〈1, 0〉}‘0) = 0) |
47 | 3, 46 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (¬ 1
= 0 → ({〈0, 0〉, 〈1, 0〉}‘0) = 0) |
48 | 45, 47 | syl5req 2657 |
. . . . . . . . . . . 12
⊢ (¬ 1
= 0 → 0 = (𝐹‘0)) |
49 | 44, 48 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (¬ 1
= 0 → (𝐹‘1) =
(𝐹‘0)) |
50 | 49 | con1i 143 |
. . . . . . . . . 10
⊢ (¬
(𝐹‘1) = (𝐹‘0) → 1 =
0) |
51 | | id 22 |
. . . . . . . . . 10
⊢ (1 = 0
→ 1 = 0) |
52 | 50, 51 | ja 172 |
. . . . . . . . 9
⊢ (((𝐹‘1) = (𝐹‘0) → 1 = 0) → 1 =
0) |
53 | 52 | ad2antrl 760 |
. . . . . . . 8
⊢
(((((𝐹‘0) =
(𝐹‘0) → 0 = 0)
∧ ((𝐹‘0) = (𝐹‘1) → 0 = 1)) ∧
(((𝐹‘1) = (𝐹‘0) → 1 = 0) ∧
((𝐹‘1) = (𝐹‘1) → 1 = 1))) →
1 = 0) |
54 | 33, 40, 53 | syl2anb 495 |
. . . . . . 7
⊢
((∀𝑦 ∈
{0, 1} ((𝐹‘0) =
(𝐹‘𝑦) → 0 = 𝑦) ∧ ∀𝑦 ∈ {0, 1} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦)) → 1 = 0) |
55 | 24, 54 | sylbi 206 |
. . . . . 6
⊢
(∀𝑥 ∈
{0, 1}∀𝑦 ∈ {0,
1} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → 1 = 0) |
56 | 55 | adantl 481 |
. . . . 5
⊢ ((𝐹:{0, 1}⟶{0, 0} ∧
∀𝑥 ∈ {0,
1}∀𝑦 ∈ {0, 1}
((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → 1 = 0) |
57 | 13, 56 | sylbi 206 |
. . . 4
⊢ (𝐹:{0, 1}–1-1→{0, 0} → 1 = 0) |
58 | 12, 57 | sylbir 224 |
. . 3
⊢ ((𝐹:{0, 1}⟶{0, 0} ∧ Fun
◡𝐹) → 1 = 0) |
59 | 11, 58 | mpan 702 |
. 2
⊢ (Fun
◡𝐹 → 1 = 0) |
60 | 2, 59 | mto 187 |
1
⊢ ¬
Fun ◡𝐹 |