Theorem dmxpss

Description: The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007)

	Ref	Expression
Assertion	dmxpss	⊢ dom ( 𝐴 × 𝐵 ) ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		xpeq2	⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
2		xp0	⊢ ( 𝐴 × ∅ ) = ∅
3	1 2	eqtrdi	⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
4	3	dmeqd	⊢ ( 𝐵 = ∅ → dom ( 𝐴 × 𝐵 ) = dom ∅ )
5		dm0	⊢ dom ∅ = ∅
6	4 5	eqtrdi	⊢ ( 𝐵 = ∅ → dom ( 𝐴 × 𝐵 ) = ∅ )
7		0ss	⊢ ∅ ⊆ 𝐴
8	6 7	eqsstrdi	⊢ ( 𝐵 = ∅ → dom ( 𝐴 × 𝐵 ) ⊆ 𝐴 )
9		dmxp	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
10		eqimss	⊢ ( dom ( 𝐴 × 𝐵 ) = 𝐴 → dom ( 𝐴 × 𝐵 ) ⊆ 𝐴 )
11	9 10	syl	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) ⊆ 𝐴 )
12	8 11	pm2.61ine	⊢ dom ( 𝐴 × 𝐵 ) ⊆ 𝐴