f1iun

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013) (Revised by Mario Carneiro, 24-Jun-2015) (Proof shortened by AV, 5-Nov-2023)

	Ref	Expression
Hypotheses	fiun.1	$⊢ x = y \to B = C$
	fiun.2	$⊢ B \in V$
Assertion	f1iun	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to ⋃_{x \in A} B : ⋃_{x \in A} D \underset{1-1}{⟶} S$

Proof

Step	Hyp	Ref	Expression
1		fiun.1	$⊢ x = y \to B = C$
2		fiun.2	$⊢ B \in V$
3		vex	$⊢ u \in V$
4		eqeq1	$⊢ z = u \to (z = B \leftrightarrow u = B)$
5	4	rexbidv	$⊢ z = u \to (\exists x \in A z = B \leftrightarrow \exists x \in A u = B)$
6	3 5	elab	$⊢ u \in \{z \| \exists x \in A z = B\} \leftrightarrow \exists x \in A u = B$
7		r19.29	$⊢ (\forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land \exists x \in A u = B) \to \exists x \in A ((B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u = B)$
8		nfv	$⊢ Ⅎ x (Fun u \land Fun u^{-1})$
9		nfre1	$⊢ Ⅎ x \exists x \in A z = B$
10	9	nfab	$⊢ \underline{Ⅎ} x \{z \| \exists x \in A z = B\}$
11		nfv	$⊢ Ⅎ x (u \subseteq v \lor v \subseteq u)$
12	10 11	nfralw	$⊢ Ⅎ x \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u)$
13	8 12	nfan	$⊢ Ⅎ x ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u))$
14		f1eq1	$⊢ u = B \to (u : D \underset{1-1}{⟶} S \leftrightarrow B : D \underset{1-1}{⟶} S)$
15	14	biimparc	$⊢ (B : D \underset{1-1}{⟶} S \land u = B) \to u : D \underset{1-1}{⟶} S$
16		df-f1	$⊢ u : D \underset{1-1}{⟶} S \leftrightarrow (u : D ⟶ S \land Fun u^{-1})$
17		ffun	$⊢ u : D ⟶ S \to Fun u$
18	17	anim1i	$⊢ (u : D ⟶ S \land Fun u^{-1}) \to (Fun u \land Fun u^{-1})$
19	16 18	sylbi	$⊢ u : D \underset{1-1}{⟶} S \to (Fun u \land Fun u^{-1})$
20	15 19	syl	$⊢ (B : D \underset{1-1}{⟶} S \land u = B) \to (Fun u \land Fun u^{-1})$
21	20	adantlr	$⊢ ((B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u = B) \to (Fun u \land Fun u^{-1})$
22		f1f	$⊢ B : D \underset{1-1}{⟶} S \to B : D ⟶ S$
23	1	fiunlem	$⊢ ((B : D ⟶ S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u = B) \to \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u)$
24	22 23	sylanl1	$⊢ ((B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u = B) \to \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u)$
25	21 24	jca	$⊢ ((B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u = B) \to ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u))$
26	25	a1i	$⊢ x \in A \to (((B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u = B) \to ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u)))$
27	13 26	rexlimi	$⊢ \exists x \in A ((B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u = B) \to ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u))$
28	7 27	syl	$⊢ (\forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land \exists x \in A u = B) \to ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u))$
29	6 28	sylan2b	$⊢ (\forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \land u \in \{z \| \exists x \in A z = B\}) \to ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u))$
30	29	ralrimiva	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to \forall u \in \{z \| \exists x \in A z = B\} ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u))$
31		fun11uni	$⊢ \forall u \in \{z \| \exists x \in A z = B\} ((Fun u \land Fun u^{-1}) \land \forall v \in \{z \| \exists x \in A z = B\} (u \subseteq v \lor v \subseteq u)) \to (Fun ⋃ \{z \| \exists x \in A z = B\} \land Fun {⋃ \{z \| \exists x \in A z = B\}}^{-1})$
32	30 31	syl	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to (Fun ⋃ \{z \| \exists x \in A z = B\} \land Fun {⋃ \{z \| \exists x \in A z = B\}}^{-1})$
33	32	simpld	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to Fun ⋃ \{z \| \exists x \in A z = B\}$
34	2	dfiun2	$⊢ ⋃_{x \in A} B = ⋃ \{z \| \exists x \in A z = B\}$
35	34	funeqi	$⊢ Fun ⋃_{x \in A} B \leftrightarrow Fun ⋃ \{z \| \exists x \in A z = B\}$
36	33 35	sylibr	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to Fun ⋃_{x \in A} B$
37	3	eldm2	$⊢ u \in dom B \leftrightarrow \exists v ⟨u, v⟩ \in B$
38		f1dm	$⊢ B : D \underset{1-1}{⟶} S \to dom B = D$
39	38	eleq2d	$⊢ B : D \underset{1-1}{⟶} S \to (u \in dom B \leftrightarrow u \in D)$
40	37 39	syl5bbr	$⊢ B : D \underset{1-1}{⟶} S \to (\exists v ⟨u, v⟩ \in B \leftrightarrow u \in D)$
41	40	adantr	$⊢ (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to (\exists v ⟨u, v⟩ \in B \leftrightarrow u \in D)$
42	41	ralrexbid	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to (\exists x \in A \exists v ⟨u, v⟩ \in B \leftrightarrow \exists x \in A u \in D)$
43		eliun	$⊢ ⟨u, v⟩ \in ⋃_{x \in A} B \leftrightarrow \exists x \in A ⟨u, v⟩ \in B$
44	43	exbii	$⊢ \exists v ⟨u, v⟩ \in ⋃_{x \in A} B \leftrightarrow \exists v \exists x \in A ⟨u, v⟩ \in B$
45	3	eldm2	$⊢ u \in dom ⋃_{x \in A} B \leftrightarrow \exists v ⟨u, v⟩ \in ⋃_{x \in A} B$
46		rexcom4	$⊢ \exists x \in A \exists v ⟨u, v⟩ \in B \leftrightarrow \exists v \exists x \in A ⟨u, v⟩ \in B$
47	44 45 46	3bitr4i	$⊢ u \in dom ⋃_{x \in A} B \leftrightarrow \exists x \in A \exists v ⟨u, v⟩ \in B$
48		eliun	$⊢ u \in ⋃_{x \in A} D \leftrightarrow \exists x \in A u \in D$
49	42 47 48	3bitr4g	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to (u \in dom ⋃_{x \in A} B \leftrightarrow u \in ⋃_{x \in A} D)$
50	49	eqrdv	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to dom ⋃_{x \in A} B = ⋃_{x \in A} D$
51		df-fn	$⊢ ⋃_{x \in A} B Fn ⋃_{x \in A} D \leftrightarrow (Fun ⋃_{x \in A} B \land dom ⋃_{x \in A} B = ⋃_{x \in A} D)$
52	36 50 51	sylanbrc	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to ⋃_{x \in A} B Fn ⋃_{x \in A} D$
53		rniun	$⊢ ran ⋃_{x \in A} B = ⋃_{x \in A} ran B$
54	22	frnd	$⊢ B : D \underset{1-1}{⟶} S \to ran B \subseteq S$
55	54	adantr	$⊢ (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to ran B \subseteq S$
56	55	ralimi	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to \forall x \in A ran B \subseteq S$
57		iunss	$⊢ ⋃_{x \in A} ran B \subseteq S \leftrightarrow \forall x \in A ran B \subseteq S$
58	56 57	sylibr	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to ⋃_{x \in A} ran B \subseteq S$
59	53 58	eqsstrid	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to ran ⋃_{x \in A} B \subseteq S$
60		df-f	$⊢ ⋃_{x \in A} B : ⋃_{x \in A} D ⟶ S \leftrightarrow (⋃_{x \in A} B Fn ⋃_{x \in A} D \land ran ⋃_{x \in A} B \subseteq S)$
61	52 59 60	sylanbrc	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to ⋃_{x \in A} B : ⋃_{x \in A} D ⟶ S$
62	32	simprd	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to Fun {⋃ \{z \| \exists x \in A z = B\}}^{-1}$
63	34	cnveqi	$⊢ {⋃_{x \in A} B}^{-1} = {⋃ \{z \| \exists x \in A z = B\}}^{-1}$
64	63	funeqi	$⊢ Fun {⋃_{x \in A} B}^{-1} \leftrightarrow Fun {⋃ \{z \| \exists x \in A z = B\}}^{-1}$
65	62 64	sylibr	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to Fun {⋃_{x \in A} B}^{-1}$
66		df-f1	$⊢ ⋃_{x \in A} B : ⋃_{x \in A} D \underset{1-1}{⟶} S \leftrightarrow (⋃_{x \in A} B : ⋃_{x \in A} D ⟶ S \land Fun {⋃_{x \in A} B}^{-1})$
67	61 65 66	sylanbrc	$⊢ \forall x \in A (B : D \underset{1-1}{⟶} S \land \forall y \in A (B \subseteq C \lor C \subseteq B)) \to ⋃_{x \in A} B : ⋃_{x \in A} D \underset{1-1}{⟶} S$

Metamath Proof Explorer

Theorem f1iun

Proof