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