Metamath Proof Explorer

Theorem founiiun

Description: Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	founiiun	$⊢ F : A \underset{onto}{⟶} B \to ⋃ B = ⋃_{x \in A} F (x)$

Proof

Step	Hyp	Ref	Expression
1		uniiun	$⊢ ⋃ B = ⋃_{y \in B} y$
2		foelrni	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to \exists x \in A F (x) = y$
3		eqimss2	$⊢ F (x) = y \to y \subseteq F (x)$
4	3	reximi	$⊢ \exists x \in A F (x) = y \to \exists x \in A y \subseteq F (x)$
5	2 4	syl	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to \exists x \in A y \subseteq F (x)$
6	5	ralrimiva	$⊢ F : A \underset{onto}{⟶} B \to \forall y \in B \exists x \in A y \subseteq F (x)$
7		iunss2	$⊢ \forall y \in B \exists x \in A y \subseteq F (x) \to ⋃_{y \in B} y \subseteq ⋃_{x \in A} F (x)$
8	6 7	syl	$⊢ F : A \underset{onto}{⟶} B \to ⋃_{y \in B} y \subseteq ⋃_{x \in A} F (x)$
9		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
10	9	ffvelrnda	$⊢ (F : A \underset{onto}{⟶} B \land x \in A) \to F (x) \in B$
11		ssidd	$⊢ (F : A \underset{onto}{⟶} B \land x \in A) \to F (x) \subseteq F (x)$
12		sseq2	$⊢ y = F (x) \to (F (x) \subseteq y \leftrightarrow F (x) \subseteq F (x))$
13	12	rspcev	$⊢ (F (x) \in B \land F (x) \subseteq F (x)) \to \exists y \in B F (x) \subseteq y$
14	10 11 13	syl2anc	$⊢ (F : A \underset{onto}{⟶} B \land x \in A) \to \exists y \in B F (x) \subseteq y$
15	14	ralrimiva	$⊢ F : A \underset{onto}{⟶} B \to \forall x \in A \exists y \in B F (x) \subseteq y$
16		iunss2	$⊢ \forall x \in A \exists y \in B F (x) \subseteq y \to ⋃_{x \in A} F (x) \subseteq ⋃_{y \in B} y$
17	15 16	syl	$⊢ F : A \underset{onto}{⟶} B \to ⋃_{x \in A} F (x) \subseteq ⋃_{y \in B} y$
18	8 17	eqssd	$⊢ F : A \underset{onto}{⟶} B \to ⋃_{y \in B} y = ⋃_{x \in A} F (x)$
19	1 18	syl5eq	$⊢ F : A \underset{onto}{⟶} B \to ⋃ B = ⋃_{x \in A} F (x)$