Metamath Proof Explorer


Theorem fun2dmnopgexmpl

Description: A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020) (Avoid depending on this detail.)

Ref Expression
Assertion fun2dmnopgexmpl ( 𝐺 = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } → ¬ 𝐺 ∈ ( V × V ) )

Proof

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 ) )