Metamath Proof Explorer

Theorem reldm

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

		Ref	Expression
	Assertion	reldm	⊢ ( Rel 𝐴 → dom 𝐴 = ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		releldm2	⊢ ( Rel 𝐴 → ( 𝑦 ∈ dom 𝐴 ↔ ∃ 𝑧 ∈ 𝐴 ( 1^st ‘ 𝑧 ) = 𝑦 ) )
2		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) )
4	2 3	fnmpti	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) Fn 𝐴
5		fvelrnb	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) Fn 𝐴 → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ‘ 𝑧 ) = 𝑦 ) )
6	4 5	ax-mp	⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ‘ 𝑧 ) = 𝑦 )
7		fveq2	⊢ ( 𝑥 = 𝑧 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑧 ) )
8		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
9	7 3 8	fvmpt	⊢ ( 𝑧 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ‘ 𝑧 ) = ( 1^st ‘ 𝑧 ) )
10	9	eqeq1d	⊢ ( 𝑧 ∈ 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ‘ 𝑧 ) = 𝑦 ↔ ( 1^st ‘ 𝑧 ) = 𝑦 ) )
11	10	rexbiia	⊢ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ∈ 𝐴 ( 1^st ‘ 𝑧 ) = 𝑦 )
12	11	a1i	⊢ ( Rel 𝐴 → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ∈ 𝐴 ( 1^st ‘ 𝑧 ) = 𝑦 ) )
13	6 12	bitr2id	⊢ ( Rel 𝐴 → ( ∃ 𝑧 ∈ 𝐴 ( 1^st ‘ 𝑧 ) = 𝑦 ↔ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ) )
14	1 13	bitrd	⊢ ( Rel 𝐴 → ( 𝑦 ∈ dom 𝐴 ↔ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ) )
15	14	eqrdv	⊢ ( Rel 𝐴 → dom 𝐴 = ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) )