Theorem djussxp2

Description: Stronger version of djussxp (Contributed by Thierry Arnoux, 23-Jun-2024)

	Ref	Expression
Assertion	djussxp2	$$⊢\bigcup _{k\in A}\left(\left\{k\right\}\times B\right)\subseteq A\times \bigcup _{k\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
2		nfiu1	$$⊢\underset{\_}{Ⅎ}k\bigcup _{k\in A}B$$
3	1 2	nfxp	$$⊢\underset{\_}{Ⅎ}k\left(A\times \bigcup _{k\in A}B\right)$$
4	3	iunssf	$$⊢\bigcup _{k\in A}\left(\left\{k\right\}\times B\right)\subseteq A\times \bigcup _{k\in A}B\leftrightarrow \forall k\in A\left\{k\right\}\times B\subseteq A\times \bigcup _{k\in A}B$$
5		snssi	$$⊢k\in A\to \left\{k\right\}\subseteq A$$
6		ssiun2	$$⊢k\in A\to B\subseteq \bigcup _{k\in A}B$$
7		xpss12	$$⊢\left(\left\{k\right\}\subseteq A\wedge B\subseteq \bigcup _{k\in A}B\right)\to \left\{k\right\}\times B\subseteq A\times \bigcup _{k\in A}B$$
8	5 6 7	syl2anc	$$⊢k\in A\to \left\{k\right\}\times B\subseteq A\times \bigcup _{k\in A}B$$
9	4 8	mprgbir	$$⊢\bigcup _{k\in A}\left(\left\{k\right\}\times B\right)\subseteq A\times \bigcup _{k\in A}B$$