Theorem fun2dmnop

Description: A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020) (Proof shortened by AV, 9-Jun-2021)

	Ref	Expression
Hypotheses	fun2dmnop.a	$$⊢A\in \mathrm{V}$$
	fun2dmnop.b	$$⊢B\in \mathrm{V}$$
Assertion	fun2dmnop	$$⊢\left(\mathrm{Fun}G\wedge A\ne B\wedge \left\{A,B\right\}\subseteq \mathrm{dom}G\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fun2dmnop.a	$$⊢A\in \mathrm{V}$$
2		fun2dmnop.b	$$⊢B\in \mathrm{V}$$
3		fundif	$$⊢\mathrm{Fun}G\to \mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)$$
4	1 2	fun2dmnop0	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge A\ne B\wedge \left\{A,B\right\}\subseteq \mathrm{dom}G\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
5	3 4	syl3an1	$$⊢\left(\mathrm{Fun}G\wedge A\ne B\wedge \left\{A,B\right\}\subseteq \mathrm{dom}G\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$