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 G /\ 2 <_ ( # ` dom G ) ) -> -. G e. ( _V X. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fundif | |- ( Fun G -> Fun ( G \ { (/) } ) ) |
|
| 2 | fundmge2nop0 | |- ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> -. G e. ( _V X. _V ) ) |
|
| 3 | 1 2 | sylan | |- ( ( Fun G /\ 2 <_ ( # ` dom G ) ) -> -. G e. ( _V X. _V ) ) |