Step | Hyp | Ref
| Expression |
1 | | 0ne1 12283 |
. . . . . . . 8
⊢ 0 ≠
1 |
2 | 1 | neii 2943 |
. . . . . . 7
⊢ ¬ 0
= 1 |
3 | 2 | intnanr 489 |
. . . . . 6
⊢ ¬ (0
= 1 ∧ 𝑎 =
{0}) |
4 | 3 | intnanr 489 |
. . . . 5
⊢ ¬
((0 = 1 ∧ 𝑎 = {0})
∧ ((0 = 1 ∧ 𝑏 = {0,
1}) ∨ (0 = 1 ∧ 𝑏 =
{0, 1}))) |
5 | 4 | gen2 1799 |
. . . 4
⊢
∀𝑎∀𝑏 ¬ ((0 = 1 ∧ 𝑎 = {0}) ∧ ((0 = 1 ∧ 𝑏 = {0, 1}) ∨ (0 = 1 ∧
𝑏 = {0,
1}))) |
6 | | eqeq1 2737 |
. . . . . . 7
⊢ (𝐺 = {⟨0, 1⟩, ⟨1,
1⟩} → (𝐺 =
⟨𝑎, 𝑏⟩ ↔ {⟨0, 1⟩, ⟨1,
1⟩} = ⟨𝑎, 𝑏⟩)) |
7 | | c0ex 11208 |
. . . . . . . 8
⊢ 0 ∈
V |
8 | | 1ex 11210 |
. . . . . . . 8
⊢ 1 ∈
V |
9 | | vex 3479 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
10 | | vex 3479 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
11 | 7, 8, 8, 8, 9, 10 | propeqop 5508 |
. . . . . . 7
⊢
({⟨0, 1⟩, ⟨1, 1⟩} = ⟨𝑎, 𝑏⟩ ↔ ((0 = 1 ∧ 𝑎 = {0}) ∧ ((0 = 1 ∧
𝑏 = {0, 1}) ∨ (0 = 1
∧ 𝑏 = {0,
1})))) |
12 | 6, 11 | bitrdi 287 |
. . . . . 6
⊢ (𝐺 = {⟨0, 1⟩, ⟨1,
1⟩} → (𝐺 =
⟨𝑎, 𝑏⟩ ↔ ((0 = 1 ∧ 𝑎 = {0}) ∧ ((0 = 1 ∧
𝑏 = {0, 1}) ∨ (0 = 1
∧ 𝑏 = {0,
1}))))) |
13 | 12 | notbid 318 |
. . . . 5
⊢ (𝐺 = {⟨0, 1⟩, ⟨1,
1⟩} → (¬ 𝐺 =
⟨𝑎, 𝑏⟩ ↔ ¬ ((0 = 1 ∧ 𝑎 = {0}) ∧ ((0 = 1 ∧
𝑏 = {0, 1}) ∨ (0 = 1
∧ 𝑏 = {0,
1}))))) |
14 | 13 | 2albidv 1927 |
. . . 4
⊢ (𝐺 = {⟨0, 1⟩, ⟨1,
1⟩} → (∀𝑎∀𝑏 ¬ 𝐺 = ⟨𝑎, 𝑏⟩ ↔ ∀𝑎∀𝑏 ¬ ((0 = 1 ∧ 𝑎 = {0}) ∧ ((0 = 1 ∧ 𝑏 = {0, 1}) ∨ (0 = 1 ∧
𝑏 = {0,
1}))))) |
15 | 5, 14 | mpbiri 258 |
. . 3
⊢ (𝐺 = {⟨0, 1⟩, ⟨1,
1⟩} → ∀𝑎∀𝑏 ¬ 𝐺 = ⟨𝑎, 𝑏⟩) |
16 | | 2nexaln 1833 |
. . 3
⊢ (¬
∃𝑎∃𝑏 𝐺 = ⟨𝑎, 𝑏⟩ ↔ ∀𝑎∀𝑏 ¬ 𝐺 = ⟨𝑎, 𝑏⟩) |
17 | 15, 16 | sylibr 233 |
. 2
⊢ (𝐺 = {⟨0, 1⟩, ⟨1,
1⟩} → ¬ ∃𝑎∃𝑏 𝐺 = ⟨𝑎, 𝑏⟩) |
18 | | elvv 5751 |
. 2
⊢ (𝐺 ∈ (V × V) ↔
∃𝑎∃𝑏 𝐺 = ⟨𝑎, 𝑏⟩) |
19 | 17, 18 | sylnibr 329 |
1
⊢ (𝐺 = {⟨0, 1⟩, ⟨1,
1⟩} → ¬ 𝐺
∈ (V × V)) |