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	⊢ ( ( Fun 𝐺 ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ¬ 𝐺 ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		fundif	⊢ ( Fun 𝐺 → Fun ( 𝐺 ∖ { ∅ } ) )
2		fundmge2nop0	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ¬ 𝐺 ∈ ( V × V ) )
3	1 2	sylan	⊢ ( ( Fun 𝐺 ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ¬ 𝐺 ∈ ( V × V ) )