This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Elementary integer functions The ` # ` (set size) function Functions with a domain containing at least two different elements 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 ) )