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 ⊢ G = 0 1 1 1 → ¬ G ∈ V × V

Proof

Step Hyp Ref Expression
1 0ne1 ⊢ 0 ≠ 1
2 1 neii ⊢ ¬ 0 = 1
3 2 intnanr ⊢ ¬ 0 = 1 ∧ a = 0
4 3 intnanr ⊢ ¬ 0 = 1 ∧ a = 0 ∧ 0 = 1 ∧ b = 0 1 ∨ 0 = 1 ∧ b = 0 1
5 4 gen2 ⊢ ∀ a ∀ b ¬ 0 = 1 ∧ a = 0 ∧ 0 = 1 ∧ b = 0 1 ∨ 0 = 1 ∧ b = 0 1
6 eqeq1 ⊢ G = 0 1 1 1 → G = a b ↔ 0 1 1 1 = a b
7 c0ex ⊢ 0 ∈ V
8 1ex ⊢ 1 ∈ V
9 vex ⊢ a ∈ V
10 vex ⊢ b ∈ V
11 7 8 8 8 9 10 propeqop ⊢ 0 1 1 1 = a b ↔ 0 = 1 ∧ a = 0 ∧ 0 = 1 ∧ b = 0 1 ∨ 0 = 1 ∧ b = 0 1
12 6 11 bitrdi ⊢ G = 0 1 1 1 → G = a b ↔ 0 = 1 ∧ a = 0 ∧ 0 = 1 ∧ b = 0 1 ∨ 0 = 1 ∧ b = 0 1
13 12 notbid ⊢ G = 0 1 1 1 → ¬ G = a b ↔ ¬ 0 = 1 ∧ a = 0 ∧ 0 = 1 ∧ b = 0 1 ∨ 0 = 1 ∧ b = 0 1
14 13 2albidv ⊢ G = 0 1 1 1 → ∀ a ∀ b ¬ G = a b ↔ ∀ a ∀ b ¬ 0 = 1 ∧ a = 0 ∧ 0 = 1 ∧ b = 0 1 ∨ 0 = 1 ∧ b = 0 1
15 5 14 mpbiri ⊢ G = 0 1 1 1 → ∀ a ∀ b ¬ G = a b
16 2nexaln ⊢ ¬ ∃ a ∃ b G = a b ↔ ∀ a ∀ b ¬ G = a b
17 15 16 sylibr ⊢ G = 0 1 1 1 → ¬ ∃ a ∃ b G = a b
18 elvv ⊢ G ∈ V × V ↔ ∃ a ∃ b G = a b
19 17 18 sylnibr ⊢ G = 0 1 1 1 → ¬ G ∈ V × V