aciunf1

Description: Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020)

	Ref	Expression
Hypotheses	aciunf1.0	$⊢ φ \to A \in V$
	aciunf1.1	$⊢ (φ \land j \in A) \to B \in W$
Assertion	aciunf1	$⊢ φ \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall k \in ⋃_{j \in A} B 2^{nd} (f (k)) = k)$

Proof

Step	Hyp	Ref	Expression
1		aciunf1.0	$⊢ φ \to A \in V$
2		aciunf1.1	$⊢ (φ \land j \in A) \to B \in W$
3		ssrab2	$⊢ \{j \in A \| B \neq \emptyset\} \subseteq A$
4		ssexg	$⊢ (\{j \in A \| B \neq \emptyset\} \subseteq A \land A \in V) \to \{j \in A \| B \neq \emptyset\} \in V$
5	3 1 4	sylancr	$⊢ φ \to \{j \in A \| B \neq \emptyset\} \in V$
6		rabid	$⊢ j \in \{j \in A \| B \neq \emptyset\} \leftrightarrow (j \in A \land B \neq \emptyset)$
7	6	biimpi	$⊢ j \in \{j \in A \| B \neq \emptyset\} \to (j \in A \land B \neq \emptyset)$
8	7	adantl	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to (j \in A \land B \neq \emptyset)$
9	8	simprd	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to B \neq \emptyset$
10		nfrab1	$⊢ \underline{Ⅎ} j \{j \in A \| B \neq \emptyset\}$
11	8	simpld	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to j \in A$
12	11 2	syldan	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to B \in W$
13	5 9 10 12	aciunf1lem	$⊢ φ \to \exists f (f : ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B \underset{1-1}{⟶} ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B) \land \forall k \in ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B 2^{nd} (f (k)) = k)$
14		eqidd	$⊢ φ \to f = f$
15		nfv	$⊢ Ⅎ j φ$
16		nfcv	$⊢ \underline{Ⅎ} j A$
17		nfrab1	$⊢ \underline{Ⅎ} j \{j \in A \| B = \emptyset\}$
18	16 17	nfdif	$⊢ \underline{Ⅎ} j (A ∖ \{j \in A \| B = \emptyset\})$
19		difrab	$⊢ \{j \in A \| ⊤\} ∖ \{j \in A \| B = \emptyset\} = \{j \in A \| (⊤ \land \neg B = \emptyset)\}$
20	16	rabtru	$⊢ \{j \in A \| ⊤\} = A$
21	20	difeq1i	$⊢ \{j \in A \| ⊤\} ∖ \{j \in A \| B = \emptyset\} = A ∖ \{j \in A \| B = \emptyset\}$
22		truan	$⊢ (⊤ \land \neg B = \emptyset) \leftrightarrow \neg B = \emptyset$
23		df-ne	$⊢ B \neq \emptyset \leftrightarrow \neg B = \emptyset$
24	22 23	bitr4i	$⊢ (⊤ \land \neg B = \emptyset) \leftrightarrow B \neq \emptyset$
25	24	rabbii	$⊢ \{j \in A \| (⊤ \land \neg B = \emptyset)\} = \{j \in A \| B \neq \emptyset\}$
26	19 21 25	3eqtr3i	$⊢ A ∖ \{j \in A \| B = \emptyset\} = \{j \in A \| B \neq \emptyset\}$
27	26	a1i	$⊢ φ \to A ∖ \{j \in A \| B = \emptyset\} = \{j \in A \| B \neq \emptyset\}$
28		eqidd	$⊢ φ \to B = B$
29	15 18 10 27 28	iuneq12df	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} B = ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B$
30		rabid	$⊢ j \in \{j \in A \| B = \emptyset\} \leftrightarrow (j \in A \land B = \emptyset)$
31	30	biimpi	$⊢ j \in \{j \in A \| B = \emptyset\} \to (j \in A \land B = \emptyset)$
32	31	adantl	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to (j \in A \land B = \emptyset)$
33	32	simprd	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to B = \emptyset$
34	33	ralrimiva	$⊢ φ \to \forall j \in \{j \in A \| B = \emptyset\} B = \emptyset$
35	17	iunxdif3	$⊢ \forall j \in \{j \in A \| B = \emptyset\} B = \emptyset \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} B = ⋃_{j \in A} B$
36	34 35	syl	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} B = ⋃_{j \in A} B$
37	29 36	eqtr3d	$⊢ φ \to ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B = ⋃_{j \in A} B$
38		eqidd	$⊢ φ \to \{j\} \times B = \{j\} \times B$
39	15 18 10 27 38	iuneq12df	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} (\{j\} \times B) = ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B)$
40	33	xpeq2d	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to \{j\} \times B = \{j\} \times \emptyset$
41		xp0	$⊢ \{j\} \times \emptyset = \emptyset$
42	40 41	eqtrdi	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to \{j\} \times B = \emptyset$
43	42	ralrimiva	$⊢ φ \to \forall j \in \{j \in A \| B = \emptyset\} \{j\} \times B = \emptyset$
44	17	iunxdif3	$⊢ \forall j \in \{j \in A \| B = \emptyset\} \{j\} \times B = \emptyset \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
45	43 44	syl	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
46	39 45	eqtr3d	$⊢ φ \to ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
47	14 37 46	f1eq123d	$⊢ φ \to (f : ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B \underset{1-1}{⟶} ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B) \leftrightarrow f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B))$
48	37	raleqdv	$⊢ φ \to (\forall k \in ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B 2^{nd} (f (k)) = k \leftrightarrow \forall k \in ⋃_{j \in A} B 2^{nd} (f (k)) = k)$
49	47 48	anbi12d	$⊢ φ \to ((f : ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B \underset{1-1}{⟶} ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B) \land \forall k \in ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B 2^{nd} (f (k)) = k) \leftrightarrow (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall k \in ⋃_{j \in A} B 2^{nd} (f (k)) = k))$
50	49	exbidv	$⊢ φ \to (\exists f (f : ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B \underset{1-1}{⟶} ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B) \land \forall k \in ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B 2^{nd} (f (k)) = k) \leftrightarrow \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall k \in ⋃_{j \in A} B 2^{nd} (f (k)) = k))$
51	13 50	mpbid	$⊢ φ \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall k \in ⋃_{j \in A} B 2^{nd} (f (k)) = k)$

Metamath Proof Explorer

Theorem aciunf1

Proof