Step |
Hyp |
Ref |
Expression |
1 |
|
1one2o |
⊢ 1o ≠ 2o |
2 |
1
|
neii |
⊢ ¬ 1o = 2o |
3 |
2
|
intnanr |
⊢ ¬ ( 1o = 2o ∧ 〈 𝑎 , 𝑏 〉 = 〈 𝑖 , 𝑢 〉 ) |
4 |
|
gonafv |
⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎 ⊼𝑔 𝑏 ) = 〈 1o , 〈 𝑎 , 𝑏 〉 〉 ) |
5 |
4
|
el2v |
⊢ ( 𝑎 ⊼𝑔 𝑏 ) = 〈 1o , 〈 𝑎 , 𝑏 〉 〉 |
6 |
|
df-goal |
⊢ ∀𝑔 𝑖 𝑢 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 |
7 |
5 6
|
eqeq12i |
⊢ ( ( 𝑎 ⊼𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ↔ 〈 1o , 〈 𝑎 , 𝑏 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 ) |
8 |
|
1oex |
⊢ 1o ∈ V |
9 |
|
opex |
⊢ 〈 𝑎 , 𝑏 〉 ∈ V |
10 |
8 9
|
opth |
⊢ ( 〈 1o , 〈 𝑎 , 𝑏 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 ↔ ( 1o = 2o ∧ 〈 𝑎 , 𝑏 〉 = 〈 𝑖 , 𝑢 〉 ) ) |
11 |
7 10
|
bitri |
⊢ ( ( 𝑎 ⊼𝑔 𝑏 ) = ∀𝑔 𝑖 𝑢 ↔ ( 1o = 2o ∧ 〈 𝑎 , 𝑏 〉 = 〈 𝑖 , 𝑢 〉 ) ) |
12 |
11
|
necon3abii |
⊢ ( ( 𝑎 ⊼𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢 ↔ ¬ ( 1o = 2o ∧ 〈 𝑎 , 𝑏 〉 = 〈 𝑖 , 𝑢 〉 ) ) |
13 |
3 12
|
mpbir |
⊢ ( 𝑎 ⊼𝑔 𝑏 ) ≠ ∀𝑔 𝑖 𝑢 |