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) (Proof shortened by SN, 23-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | relssdmrn | ⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | ⊢ ( Rel 𝐴 → Rel 𝐴 ) | |
| 2 | vex | ⊢ 𝑥 ∈ V | |
| 3 | vex | ⊢ 𝑦 ∈ V | |
| 4 | 2 3 | opeldm | ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴 ) |
| 5 | 2 3 | opelrn | ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 ∈ ran 𝐴 ) |
| 6 | 4 5 | opelxpd | ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ) |
| 7 | 6 | a1i | ⊢ ( Rel 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ) ) |
| 8 | 1 7 | relssdv | ⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) ) |