funopdmsn

Description: The domain of a function which is an ordered pair is a singleton. (Contributed by AV, 15-Nov-2021) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	funopdmsn.g	$⊢ G = ⟨X, Y⟩$
	funopdmsn.x	$⊢ X \in V$
	funopdmsn.y	$⊢ Y \in W$
Assertion	funopdmsn	$⊢ (Fun G \land A \in dom G \land B \in dom G) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		funopdmsn.g	$⊢ G = ⟨X, Y⟩$
2		funopdmsn.x	$⊢ X \in V$
3		funopdmsn.y	$⊢ Y \in W$
4	1	funeqi	$⊢ Fun G \leftrightarrow Fun ⟨X, Y⟩$
5	2	elexi	$⊢ X \in V$
6	3	elexi	$⊢ Y \in V$
7	5 6	funop	$⊢ Fun ⟨X, Y⟩ \leftrightarrow \exists x (X = \{x\} \land ⟨X, Y⟩ = \{⟨x, x⟩\})$
8	4 7	bitri	$⊢ Fun G \leftrightarrow \exists x (X = \{x\} \land ⟨X, Y⟩ = \{⟨x, x⟩\})$
9	1	eqcomi	$⊢ ⟨X, Y⟩ = G$
10	9	eqeq1i	$⊢ ⟨X, Y⟩ = \{⟨x, x⟩\} \leftrightarrow G = \{⟨x, x⟩\}$
11		dmeq	$⊢ G = \{⟨x, x⟩\} \to dom G = dom \{⟨x, x⟩\}$
12		vex	$⊢ x \in V$
13	12	dmsnop	$⊢ dom \{⟨x, x⟩\} = \{x\}$
14	11 13	eqtrdi	$⊢ G = \{⟨x, x⟩\} \to dom G = \{x\}$
15		eleq2	$⊢ dom G = \{x\} \to (A \in dom G \leftrightarrow A \in \{x\})$
16		eleq2	$⊢ dom G = \{x\} \to (B \in dom G \leftrightarrow B \in \{x\})$
17	15 16	anbi12d	$⊢ dom G = \{x\} \to ((A \in dom G \land B \in dom G) \leftrightarrow (A \in \{x\} \land B \in \{x\}))$
18		elsni	$⊢ A \in \{x\} \to A = x$
19		elsni	$⊢ B \in \{x\} \to B = x$
20		eqtr3	$⊢ (A = x \land B = x) \to A = B$
21	18 19 20	syl2an	$⊢ (A \in \{x\} \land B \in \{x\}) \to A = B$
22	17 21	biimtrdi	$⊢ dom G = \{x\} \to ((A \in dom G \land B \in dom G) \to A = B)$
23	14 22	syl	$⊢ G = \{⟨x, x⟩\} \to ((A \in dom G \land B \in dom G) \to A = B)$
24	10 23	sylbi	$⊢ ⟨X, Y⟩ = \{⟨x, x⟩\} \to ((A \in dom G \land B \in dom G) \to A = B)$
25	24	adantl	$⊢ (X = \{x\} \land ⟨X, Y⟩ = \{⟨x, x⟩\}) \to ((A \in dom G \land B \in dom G) \to A = B)$
26	25	exlimiv	$⊢ \exists x (X = \{x\} \land ⟨X, Y⟩ = \{⟨x, x⟩\}) \to ((A \in dom G \land B \in dom G) \to A = B)$
27	8 26	sylbi	$⊢ Fun G \to ((A \in dom G \land B \in dom G) \to A = B)$
28	27	3impib	$⊢ (Fun G \land A \in dom G \land B \in dom G) \to A = B$

Metamath Proof Explorer

Theorem funopdmsn

Proof