Description: The domain of a Cartesian product. Part of Theorem 3.13(x) of Monk1 p. 37. (Contributed by NM, 28-Jul-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dmxp | ⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-xp | ⊢ ( 𝐴 × 𝐵 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } | |
| 2 | 1 | dmeqi | ⊢ dom ( 𝐴 × 𝐵 ) = dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } |
| 3 | n0 | ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 ) | |
| 4 | 3 | biimpi | ⊢ ( 𝐵 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐵 ) |
| 5 | 4 | ralrimivw | ⊢ ( 𝐵 ≠ ∅ → ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 𝑥 ∈ 𝐵 ) |
| 6 | dmopab3 | ⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 𝑥 ∈ 𝐵 ↔ dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } = 𝐴 ) | |
| 7 | 5 6 | sylib | ⊢ ( 𝐵 ≠ ∅ → dom { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } = 𝐴 ) |
| 8 | 2 7 | syl5eq | ⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 ) |