founiiun0

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

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

Proof

Step	Hyp	Ref	Expression
1		uniiun	$⊢ ⋃ B = ⋃_{y \in B} y$
2		elun1	$⊢ y \in B \to y \in (B \cup \{\emptyset\})$
3		foelcdmi	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land y \in (B \cup \{\emptyset\})) \to \exists x \in A F (x) = y$
4	2 3	sylan2	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land y \in B) \to \exists x \in A F (x) = y$
5		eqimss2	$⊢ F (x) = y \to y \subseteq F (x)$
6	5	reximi	$⊢ \exists x \in A F (x) = y \to \exists x \in A y \subseteq F (x)$
7	4 6	syl	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land y \in B) \to \exists x \in A y \subseteq F (x)$
8	7	ralrimiva	$⊢ F : A \underset{onto}{⟶} B \cup \{\emptyset\} \to \forall y \in B \exists x \in A y \subseteq F (x)$
9		iunss2	$⊢ \forall y \in B \exists x \in A y \subseteq F (x) \to ⋃_{y \in B} y \subseteq ⋃_{x \in A} F (x)$
10	8 9	syl	$⊢ F : A \underset{onto}{⟶} B \cup \{\emptyset\} \to ⋃_{y \in B} y \subseteq ⋃_{x \in A} F (x)$
11		simpl	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land B = \emptyset) \to F : A \underset{onto}{⟶} B \cup \{\emptyset\}$
12		uneq1	$⊢ B = \emptyset \to B \cup \{\emptyset\} = \emptyset \cup \{\emptyset\}$
13		0un	$⊢ \emptyset \cup \{\emptyset\} = \{\emptyset\}$
14	12 13	eqtrdi	$⊢ B = \emptyset \to B \cup \{\emptyset\} = \{\emptyset\}$
15	14	adantl	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land B = \emptyset) \to B \cup \{\emptyset\} = \{\emptyset\}$
16		foeq3	$⊢ B \cup \{\emptyset\} = \{\emptyset\} \to (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \leftrightarrow F : A \underset{onto}{⟶} \{\emptyset\})$
17	15 16	syl	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land B = \emptyset) \to (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \leftrightarrow F : A \underset{onto}{⟶} \{\emptyset\})$
18	11 17	mpbid	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land B = \emptyset) \to F : A \underset{onto}{⟶} \{\emptyset\}$
19		founiiun	$⊢ F : A \underset{onto}{⟶} \{\emptyset\} \to ⋃ \{\emptyset\} = ⋃_{x \in A} F (x)$
20		unisn0	$⊢ ⋃ \{\emptyset\} = \emptyset$
21	19 20	eqtr3di	$⊢ F : A \underset{onto}{⟶} \{\emptyset\} \to ⋃_{x \in A} F (x) = \emptyset$
22		0ss	$⊢ \emptyset \subseteq ⋃_{y \in B} y$
23	21 22	eqsstrdi	$⊢ F : A \underset{onto}{⟶} \{\emptyset\} \to ⋃_{x \in A} F (x) \subseteq ⋃_{y \in B} y$
24	18 23	syl	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land B = \emptyset) \to ⋃_{x \in A} F (x) \subseteq ⋃_{y \in B} y$
25		ssid	$⊢ F (x) \subseteq F (x)$
26		sseq2	$⊢ y = F (x) \to (F (x) \subseteq y \leftrightarrow F (x) \subseteq F (x))$
27	26	rspcev	$⊢ (F (x) \in B \land F (x) \subseteq F (x)) \to \exists y \in B F (x) \subseteq y$
28	25 27	mpan2	$⊢ F (x) \in B \to \exists y \in B F (x) \subseteq y$
29	28	adantl	$⊢ (((F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land \neg B = \emptyset) \land x \in A) \land F (x) \in B) \to \exists y \in B F (x) \subseteq y$
30		fof	$⊢ F : A \underset{onto}{⟶} B \cup \{\emptyset\} \to F : A ⟶ B \cup \{\emptyset\}$
31	30	ffvelcdmda	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land x \in A) \to F (x) \in (B \cup \{\emptyset\})$
32		elunnel1	$⊢ (F (x) \in (B \cup \{\emptyset\}) \land \neg F (x) \in B) \to F (x) \in \{\emptyset\}$
33	31 32	sylan	$⊢ ((F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land x \in A) \land \neg F (x) \in B) \to F (x) \in \{\emptyset\}$
34		elsni	$⊢ F (x) \in \{\emptyset\} \to F (x) = \emptyset$
35	33 34	syl	$⊢ ((F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land x \in A) \land \neg F (x) \in B) \to F (x) = \emptyset$
36	35	adantllr	$⊢ (((F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land \neg B = \emptyset) \land x \in A) \land \neg F (x) \in B) \to F (x) = \emptyset$
37		neq0	$⊢ \neg B = \emptyset \leftrightarrow \exists y y \in B$
38	37	birani	$⊢ (\neg B = \emptyset \land F (x) = \emptyset) \to \exists y y \in B$
39		id	$⊢ F (x) = \emptyset \to F (x) = \emptyset$
40		0ss	$⊢ \emptyset \subseteq y$
41	39 40	eqsstrdi	$⊢ F (x) = \emptyset \to F (x) \subseteq y$
42	41	anim1ci	$⊢ (F (x) = \emptyset \land y \in B) \to (y \in B \land F (x) \subseteq y)$
43	42	ex	$⊢ F (x) = \emptyset \to (y \in B \to (y \in B \land F (x) \subseteq y))$
44	43	adantl	$⊢ (\neg B = \emptyset \land F (x) = \emptyset) \to (y \in B \to (y \in B \land F (x) \subseteq y))$
45	44	eximdv	$⊢ (\neg B = \emptyset \land F (x) = \emptyset) \to (\exists y y \in B \to \exists y (y \in B \land F (x) \subseteq y))$
46	38 45	mpd	$⊢ (\neg B = \emptyset \land F (x) = \emptyset) \to \exists y (y \in B \land F (x) \subseteq y)$
47		df-rex	$⊢ \exists y \in B F (x) \subseteq y \leftrightarrow \exists y (y \in B \land F (x) \subseteq y)$
48	46 47	sylibr	$⊢ (\neg B = \emptyset \land F (x) = \emptyset) \to \exists y \in B F (x) \subseteq y$
49	48	ad4ant24	$⊢ (((F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land \neg B = \emptyset) \land x \in A) \land F (x) = \emptyset) \to \exists y \in B F (x) \subseteq y$
50	36 49	syldan	$⊢ (((F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land \neg B = \emptyset) \land x \in A) \land \neg F (x) \in B) \to \exists y \in B F (x) \subseteq y$
51	29 50	pm2.61dan	$⊢ ((F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land \neg B = \emptyset) \land x \in A) \to \exists y \in B F (x) \subseteq y$
52	51	ralrimiva	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land \neg B = \emptyset) \to \forall x \in A \exists y \in B F (x) \subseteq y$
53		iunss2	$⊢ \forall x \in A \exists y \in B F (x) \subseteq y \to ⋃_{x \in A} F (x) \subseteq ⋃_{y \in B} y$
54	52 53	syl	$⊢ (F : A \underset{onto}{⟶} B \cup \{\emptyset\} \land \neg B = \emptyset) \to ⋃_{x \in A} F (x) \subseteq ⋃_{y \in B} y$
55	24 54	pm2.61dan	$⊢ F : A \underset{onto}{⟶} B \cup \{\emptyset\} \to ⋃_{x \in A} F (x) \subseteq ⋃_{y \in B} y$
56	10 55	eqssd	$⊢ F : A \underset{onto}{⟶} B \cup \{\emptyset\} \to ⋃_{y \in B} y = ⋃_{x \in A} F (x)$
57	1 56	eqtrid	$⊢ F : A \underset{onto}{⟶} B \cup \{\emptyset\} \to ⋃ B = ⋃_{x \in A} F (x)$

Metamath Proof Explorer

Theorem founiiun0

Proof