djussxp2

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

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

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

Metamath Proof Explorer