Step |
Hyp |
Ref |
Expression |
1 |
|
0ne1 |
⊢ 0 ≠ 1 |
2 |
1
|
neii |
⊢ ¬ 0 = 1 |
3 |
2
|
intnanr |
⊢ ¬ ( 0 = 1 ∧ 𝑎 = { 0 } ) |
4 |
3
|
intnanr |
⊢ ¬ ( ( 0 = 1 ∧ 𝑎 = { 0 } ) ∧ ( ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ∨ ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ) ) |
5 |
4
|
gen2 |
⊢ ∀ 𝑎 ∀ 𝑏 ¬ ( ( 0 = 1 ∧ 𝑎 = { 0 } ) ∧ ( ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ∨ ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ) ) |
6 |
|
eqeq1 |
⊢ ( 𝐺 = { 〈 0 , 1 〉 , 〈 1 , 1 〉 } → ( 𝐺 = 〈 𝑎 , 𝑏 〉 ↔ { 〈 0 , 1 〉 , 〈 1 , 1 〉 } = 〈 𝑎 , 𝑏 〉 ) ) |
7 |
|
c0ex |
⊢ 0 ∈ V |
8 |
|
1ex |
⊢ 1 ∈ V |
9 |
|
vex |
⊢ 𝑎 ∈ V |
10 |
|
vex |
⊢ 𝑏 ∈ V |
11 |
7 8 8 8 9 10
|
propeqop |
⊢ ( { 〈 0 , 1 〉 , 〈 1 , 1 〉 } = 〈 𝑎 , 𝑏 〉 ↔ ( ( 0 = 1 ∧ 𝑎 = { 0 } ) ∧ ( ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ∨ ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ) ) ) |
12 |
6 11
|
bitrdi |
⊢ ( 𝐺 = { 〈 0 , 1 〉 , 〈 1 , 1 〉 } → ( 𝐺 = 〈 𝑎 , 𝑏 〉 ↔ ( ( 0 = 1 ∧ 𝑎 = { 0 } ) ∧ ( ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ∨ ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ) ) ) ) |
13 |
12
|
notbid |
⊢ ( 𝐺 = { 〈 0 , 1 〉 , 〈 1 , 1 〉 } → ( ¬ 𝐺 = 〈 𝑎 , 𝑏 〉 ↔ ¬ ( ( 0 = 1 ∧ 𝑎 = { 0 } ) ∧ ( ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ∨ ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ) ) ) ) |
14 |
13
|
2albidv |
⊢ ( 𝐺 = { 〈 0 , 1 〉 , 〈 1 , 1 〉 } → ( ∀ 𝑎 ∀ 𝑏 ¬ 𝐺 = 〈 𝑎 , 𝑏 〉 ↔ ∀ 𝑎 ∀ 𝑏 ¬ ( ( 0 = 1 ∧ 𝑎 = { 0 } ) ∧ ( ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ∨ ( 0 = 1 ∧ 𝑏 = { 0 , 1 } ) ) ) ) ) |
15 |
5 14
|
mpbiri |
⊢ ( 𝐺 = { 〈 0 , 1 〉 , 〈 1 , 1 〉 } → ∀ 𝑎 ∀ 𝑏 ¬ 𝐺 = 〈 𝑎 , 𝑏 〉 ) |
16 |
|
2nexaln |
⊢ ( ¬ ∃ 𝑎 ∃ 𝑏 𝐺 = 〈 𝑎 , 𝑏 〉 ↔ ∀ 𝑎 ∀ 𝑏 ¬ 𝐺 = 〈 𝑎 , 𝑏 〉 ) |
17 |
15 16
|
sylibr |
⊢ ( 𝐺 = { 〈 0 , 1 〉 , 〈 1 , 1 〉 } → ¬ ∃ 𝑎 ∃ 𝑏 𝐺 = 〈 𝑎 , 𝑏 〉 ) |
18 |
|
elvv |
⊢ ( 𝐺 ∈ ( V × V ) ↔ ∃ 𝑎 ∃ 𝑏 𝐺 = 〈 𝑎 , 𝑏 〉 ) |
19 |
17 18
|
sylnibr |
⊢ ( 𝐺 = { 〈 0 , 1 〉 , 〈 1 , 1 〉 } → ¬ 𝐺 ∈ ( V × V ) ) |