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	bilani	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to (j \in A \land B \neq \emptyset)$
8	7	simprd	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to B \neq \emptyset$
9		nfrab1	$⊢ \underline{Ⅎ} j \{j \in A \| B \neq \emptyset\}$
10	7	simpld	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to j \in A$
11	10 2	syldan	$⊢ (φ \land j \in \{j \in A \| B \neq \emptyset\}) \to B \in W$
12	5 8 9 11	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)$
13		eqidd	$⊢ φ \to f = f$
14		nfv	$⊢ Ⅎ j φ$
15		nfcv	$⊢ \underline{Ⅎ} j A$
16		nfrab1	$⊢ \underline{Ⅎ} j \{j \in A \| B = \emptyset\}$
17	15 16	nfdif	$⊢ \underline{Ⅎ} j (A ∖ \{j \in A \| B = \emptyset\})$
18		difrab	$⊢ \{j \in A \| ⊤\} ∖ \{j \in A \| B = \emptyset\} = \{j \in A \| (⊤ \land \neg B = \emptyset)\}$
19	15	rabtru	$⊢ \{j \in A \| ⊤\} = A$
20	19	difeq1i	$⊢ \{j \in A \| ⊤\} ∖ \{j \in A \| B = \emptyset\} = A ∖ \{j \in A \| B = \emptyset\}$
21		truan	$⊢ (⊤ \land \neg B = \emptyset) \leftrightarrow \neg B = \emptyset$
22		df-ne	$⊢ B \neq \emptyset \leftrightarrow \neg B = \emptyset$
23	21 22	bitr4i	$⊢ (⊤ \land \neg B = \emptyset) \leftrightarrow B \neq \emptyset$
24	23	rabbii	$⊢ \{j \in A \| (⊤ \land \neg B = \emptyset)\} = \{j \in A \| B \neq \emptyset\}$
25	18 20 24	3eqtr3i	$⊢ A ∖ \{j \in A \| B = \emptyset\} = \{j \in A \| B \neq \emptyset\}$
26	25	a1i	$⊢ φ \to A ∖ \{j \in A \| B = \emptyset\} = \{j \in A \| B \neq \emptyset\}$
27		eqidd	$⊢ φ \to B = B$
28	14 17 9 26 27	iuneq12df	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} B = ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B$
29		rabid	$⊢ j \in \{j \in A \| B = \emptyset\} \leftrightarrow (j \in A \land B = \emptyset)$
30	29	bilani	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to (j \in A \land B = \emptyset)$
31	30	simprd	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to B = \emptyset$
32	31	ralrimiva	$⊢ φ \to \forall j \in \{j \in A \| B = \emptyset\} B = \emptyset$
33	16	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$
34	32 33	syl	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} B = ⋃_{j \in A} B$
35	28 34	eqtr3d	$⊢ φ \to ⋃_{j \in \{j \in A \| B \neq \emptyset\}} B = ⋃_{j \in A} B$
36		eqidd	$⊢ φ \to \{j\} \times B = \{j\} \times B$
37	14 17 9 26 36	iuneq12df	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} (\{j\} \times B) = ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B)$
38	31	xpeq2d	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to \{j\} \times B = \{j\} \times \emptyset$
39		xp0	$⊢ \{j\} \times \emptyset = \emptyset$
40	38 39	eqtrdi	$⊢ (φ \land j \in \{j \in A \| B = \emptyset\}) \to \{j\} \times B = \emptyset$
41	40	ralrimiva	$⊢ φ \to \forall j \in \{j \in A \| B = \emptyset\} \{j\} \times B = \emptyset$
42	16	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)$
43	41 42	syl	$⊢ φ \to ⋃_{j \in A ∖ \{j \in A \| B = \emptyset\}} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
44	37 43	eqtr3d	$⊢ φ \to ⋃_{j \in \{j \in A \| B \neq \emptyset\}} (\{j\} \times B) = ⋃_{j \in A} (\{j\} \times B)$
45	13 35 44	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))$
46	35	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)$
47	45 46	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))$
48	47	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))$
49	12 48	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