fun2dmnop0

Description: A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop (with the less restrictive requirement that ( G \ { (/) } ) needs to be a function instead of G ) is useful for proofs for extensible structures, see structn0fun . (Contributed by AV, 21-Sep-2020) (Revised by AV, 7-Jun-2021)

	Ref	Expression
Hypotheses	fun2dmnop.a	$⊢ A \in V$
	fun2dmnop.b	$⊢ B \in V$
Assertion	fun2dmnop0	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to \neg G \in (V \times V)$

Proof

Step	Hyp	Ref	Expression
1		fun2dmnop.a	$⊢ A \in V$
2		fun2dmnop.b	$⊢ B \in V$
3		simpl1	$⊢ ((Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \land G \in V) \to Fun (G ∖ \{\emptyset\})$
4		dmexg	$⊢ G \in V \to dom G \in V$
5	4	adantl	$⊢ ((Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \land G \in V) \to dom G \in V$
6	1 2	prss	$⊢ (A \in dom G \land B \in dom G) \leftrightarrow \{A, B\} \subseteq dom G$
7		simpl	$⊢ (A \in dom G \land B \in dom G) \to A \in dom G$
8	6 7	sylbir	$⊢ \{A, B\} \subseteq dom G \to A \in dom G$
9	8	3ad2ant3	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to A \in dom G$
10	9	adantr	$⊢ ((Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \land G \in V) \to A \in dom G$
11		simpr	$⊢ (A \in dom G \land B \in dom G) \to B \in dom G$
12	6 11	sylbir	$⊢ \{A, B\} \subseteq dom G \to B \in dom G$
13	12	3ad2ant3	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to B \in dom G$
14	13	adantr	$⊢ ((Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \land G \in V) \to B \in dom G$
15		simpl2	$⊢ ((Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \land G \in V) \to A \neq B$
16	5 10 14 15	nehash2	$⊢ ((Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \land G \in V) \to 2 \leq \|dom G\|$
17		fundmge2nop0	$⊢ (Fun (G ∖ \{\emptyset\}) \land 2 \leq \|dom G\|) \to \neg G \in (V \times V)$
18	3 16 17	syl2anc	$⊢ ((Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \land G \in V) \to \neg G \in (V \times V)$
19	18	ex	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to (G \in V \to \neg G \in (V \times V))$
20		prcnel	$⊢ \neg G \in V \to \neg G \in (V \times V)$
21	19 20	pm2.61d1	$⊢ (Fun (G ∖ \{\emptyset\}) \land A \neq B \land \{A, B\} \subseteq dom G) \to \neg G \in (V \times V)$

Metamath Proof Explorer

Theorem fun2dmnop0

Proof