Theorem fundmge2nop

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

	Ref	Expression
Assertion	fundmge2nop	$$⊢\left(\mathrm{Fun}G\wedge 2\le \left|\mathrm{dom}G\right|\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fundif	$$⊢\mathrm{Fun}G\to \mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)$$
2		fundmge2nop0	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge 2\le \left|\mathrm{dom}G\right|\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
3	1 2	sylan	$$⊢\left(\mathrm{Fun}G\wedge 2\le \left|\mathrm{dom}G\right|\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$