fundmge2nop0

Description: A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop (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, 12-Oct-2020) (Revised by AV, 7-Jun-2021) (Proof shortened by AV, 15-Nov-2021)

		Ref	Expression
	Assertion	fundmge2nop0	$⊢ (Fun (G ∖ \{\emptyset\}) \land 2 \leq \|dom G\|) \to \neg G \in (V \times V)$

Proof

Step	Hyp	Ref	Expression
1		dmexg	$⊢ G \in V \to dom G \in V$
2		hashge2el2dif	$⊢ (dom G \in V \land 2 \leq \|dom G\|) \to \exists a \in dom G \exists b \in dom G a \neq b$
3	2	ex	$⊢ dom G \in V \to (2 \leq \|dom G\| \to \exists a \in dom G \exists b \in dom G a \neq b)$
4	1 3	syl	$⊢ G \in V \to (2 \leq \|dom G\| \to \exists a \in dom G \exists b \in dom G a \neq b)$
5		df-ne	$⊢ a \neq b \leftrightarrow \neg a = b$
6		elvv	$⊢ G \in (V \times V) \leftrightarrow \exists x \exists y G = ⟨x, y⟩$
7		difeq1	$⊢ G = ⟨x, y⟩ \to G ∖ \{\emptyset\} = ⟨x, y⟩ ∖ \{\emptyset\}$
8	7	funeqd	$⊢ G = ⟨x, y⟩ \to (Fun (G ∖ \{\emptyset\}) \leftrightarrow Fun (⟨x, y⟩ ∖ \{\emptyset\}))$
9		opwo0id	$⊢ ⟨x, y⟩ = ⟨x, y⟩ ∖ \{\emptyset\}$
10	9	eqcomi	$⊢ ⟨x, y⟩ ∖ \{\emptyset\} = ⟨x, y⟩$
11	10	funeqi	$⊢ Fun (⟨x, y⟩ ∖ \{\emptyset\}) \leftrightarrow Fun ⟨x, y⟩$
12		dmeq	$⊢ G = ⟨x, y⟩ \to dom G = dom ⟨x, y⟩$
13	12	eleq2d	$⊢ G = ⟨x, y⟩ \to (a \in dom G \leftrightarrow a \in dom ⟨x, y⟩)$
14	12	eleq2d	$⊢ G = ⟨x, y⟩ \to (b \in dom G \leftrightarrow b \in dom ⟨x, y⟩)$
15	13 14	anbi12d	$⊢ G = ⟨x, y⟩ \to ((a \in dom G \land b \in dom G) \leftrightarrow (a \in dom ⟨x, y⟩ \land b \in dom ⟨x, y⟩))$
16		eqid	$⊢ ⟨x, y⟩ = ⟨x, y⟩$
17		vex	$⊢ x \in V$
18		vex	$⊢ y \in V$
19	16 17 18	funopdmsn	$⊢ (Fun ⟨x, y⟩ \land a \in dom ⟨x, y⟩ \land b \in dom ⟨x, y⟩) \to a = b$
20	19	3expb	$⊢ (Fun ⟨x, y⟩ \land (a \in dom ⟨x, y⟩ \land b \in dom ⟨x, y⟩)) \to a = b$
21	20	expcom	$⊢ (a \in dom ⟨x, y⟩ \land b \in dom ⟨x, y⟩) \to (Fun ⟨x, y⟩ \to a = b)$
22	15 21	syl6bi	$⊢ G = ⟨x, y⟩ \to ((a \in dom G \land b \in dom G) \to (Fun ⟨x, y⟩ \to a = b))$
23	22	com23	$⊢ G = ⟨x, y⟩ \to (Fun ⟨x, y⟩ \to ((a \in dom G \land b \in dom G) \to a = b))$
24	11 23	syl5bi	$⊢ G = ⟨x, y⟩ \to (Fun (⟨x, y⟩ ∖ \{\emptyset\}) \to ((a \in dom G \land b \in dom G) \to a = b))$
25	8 24	sylbid	$⊢ G = ⟨x, y⟩ \to (Fun (G ∖ \{\emptyset\}) \to ((a \in dom G \land b \in dom G) \to a = b))$
26	25	impcomd	$⊢ G = ⟨x, y⟩ \to (((a \in dom G \land b \in dom G) \land Fun (G ∖ \{\emptyset\})) \to a = b)$
27	26	exlimivv	$⊢ \exists x \exists y G = ⟨x, y⟩ \to (((a \in dom G \land b \in dom G) \land Fun (G ∖ \{\emptyset\})) \to a = b)$
28	27	com12	$⊢ ((a \in dom G \land b \in dom G) \land Fun (G ∖ \{\emptyset\})) \to (\exists x \exists y G = ⟨x, y⟩ \to a = b)$
29	6 28	syl5bi	$⊢ ((a \in dom G \land b \in dom G) \land Fun (G ∖ \{\emptyset\})) \to (G \in (V \times V) \to a = b)$
30	29	con3d	$⊢ ((a \in dom G \land b \in dom G) \land Fun (G ∖ \{\emptyset\})) \to (\neg a = b \to \neg G \in (V \times V))$
31	30	ex	$⊢ (a \in dom G \land b \in dom G) \to (Fun (G ∖ \{\emptyset\}) \to (\neg a = b \to \neg G \in (V \times V)))$
32	31	com23	$⊢ (a \in dom G \land b \in dom G) \to (\neg a = b \to (Fun (G ∖ \{\emptyset\}) \to \neg G \in (V \times V)))$
33	5 32	syl5bi	$⊢ (a \in dom G \land b \in dom G) \to (a \neq b \to (Fun (G ∖ \{\emptyset\}) \to \neg G \in (V \times V)))$
34	33	rexlimivv	$⊢ \exists a \in dom G \exists b \in dom G a \neq b \to (Fun (G ∖ \{\emptyset\}) \to \neg G \in (V \times V))$
35	4 34	syl6	$⊢ G \in V \to (2 \leq \|dom G\| \to (Fun (G ∖ \{\emptyset\}) \to \neg G \in (V \times V)))$
36	35	com13	$⊢ Fun (G ∖ \{\emptyset\}) \to (2 \leq \|dom G\| \to (G \in V \to \neg G \in (V \times V)))$
37	36	imp	$⊢ (Fun (G ∖ \{\emptyset\}) \land 2 \leq \|dom G\|) \to (G \in V \to \neg G \in (V \times V))$
38		prcnel	$⊢ \neg G \in V \to \neg G \in (V \times V)$
39	37 38	pm2.61d1	$⊢ (Fun (G ∖ \{\emptyset\}) \land 2 \leq \|dom G\|) \to \neg G \in (V \times V)$

Metamath Proof Explorer

Theorem fundmge2nop0

Proof