Theorem relssdmrn

Description: A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of Mendelson p. 235. (Contributed by NM, 3-Aug-1994)

	Ref	Expression
Assertion	relssdmrn	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( Rel 𝐴 → Rel 𝐴 )
2		19.8a	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3		19.8a	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
4		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) )
5		vex	⊢ 𝑥 ∈ V
6	5	eldm2	⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
7		vex	⊢ 𝑦 ∈ V
8	7	elrn2	⊢ ( 𝑦 ∈ ran 𝐴 ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
9	6 8	anbi12i	⊢ ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑦 ∈ ran 𝐴 ) ↔ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
10	4 9	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ↔ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
11	2 3 10	sylanbrc	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) )
12	11	a1i	⊢ ( Rel 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ) )
13	1 12	relssdv	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )