reldm

Description: An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013)

		Ref	Expression
	Assertion	reldm	$⊢ Rel A \to dom A = ran (x \in A ⟼ 1^{st} (x))$

Step	Hyp	Ref	Expression
1		releldm2	$⊢ Rel A \to (y \in dom A \leftrightarrow \exists z \in A 1^{st} (z) = y)$
2		fvex	$⊢ 1^{st} (x) \in V$
3		eqid	$⊢ (x \in A ⟼ 1^{st} (x)) = (x \in A ⟼ 1^{st} (x))$
4	2 3	fnmpti	$⊢ (x \in A ⟼ 1^{st} (x)) Fn A$
5		fvelrnb	$⊢ (x \in A ⟼ 1^{st} (x)) Fn A \to (y \in ran (x \in A ⟼ 1^{st} (x)) \leftrightarrow \exists z \in A (x \in A ⟼ 1^{st} (x)) (z) = y)$
6	4 5	ax-mp	$⊢ y \in ran (x \in A ⟼ 1^{st} (x)) \leftrightarrow \exists z \in A (x \in A ⟼ 1^{st} (x)) (z) = y$
7		fveq2	$⊢ x = z \to 1^{st} (x) = 1^{st} (z)$
8		fvex	$⊢ 1^{st} (z) \in V$
9	7 3 8	fvmpt	$⊢ z \in A \to (x \in A ⟼ 1^{st} (x)) (z) = 1^{st} (z)$
10	9	eqeq1d	$⊢ z \in A \to ((x \in A ⟼ 1^{st} (x)) (z) = y \leftrightarrow 1^{st} (z) = y)$
11	10	rexbiia	$⊢ \exists z \in A (x \in A ⟼ 1^{st} (x)) (z) = y \leftrightarrow \exists z \in A 1^{st} (z) = y$
12	11	a1i	$⊢ Rel A \to (\exists z \in A (x \in A ⟼ 1^{st} (x)) (z) = y \leftrightarrow \exists z \in A 1^{st} (z) = y)$
13	6 12	bitr2id	$⊢ Rel A \to (\exists z \in A 1^{st} (z) = y \leftrightarrow y \in ran (x \in A ⟼ 1^{st} (x)))$
14	1 13	bitrd	$⊢ Rel A \to (y \in dom A \leftrightarrow y \in ran (x \in A ⟼ 1^{st} (x)))$
15	14	eqrdv	$⊢ Rel A \to dom A = ran (x \in A ⟼ 1^{st} (x))$

Metamath Proof Explorer