Theorem disjsnxp

Description: The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	disjsnxp	$$⊢\underset{j\in A}{Disj}\left(\left\{j\right\}\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sndisj	$$⊢\underset{j\in A}{Disj}\left\{j\right\}$$
2	1	a1i	$$⊢\top \to \underset{j\in A}{Disj}\left\{j\right\}$$
3	2	disjxp1	$$⊢\top \to \underset{j\in A}{Disj}\left(\left\{j\right\}\times B\right)$$
4	3	mptru	$$⊢\underset{j\in A}{Disj}\left(\left\{j\right\}\times B\right)$$