Theorem djussxp

Description: Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014)

	Ref	Expression
Assertion	djussxp	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⊆ ( 𝐴 × V )

Proof

Step	Hyp	Ref	Expression
1		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⊆ ( 𝐴 × V ) ↔ ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⊆ ( 𝐴 × V ) )
2		snssi	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ 𝐴 )
3		ssv	⊢ 𝐵 ⊆ V
4		xpss12	⊢ ( ( { 𝑥 } ⊆ 𝐴 ∧ 𝐵 ⊆ V ) → ( { 𝑥 } × 𝐵 ) ⊆ ( 𝐴 × V ) )
5	2 3 4	sylancl	⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } × 𝐵 ) ⊆ ( 𝐴 × V ) )
6	1 5	mprgbir	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⊆ ( 𝐴 × V )