aciunf1lem

Description: Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019)

	Ref	Expression
Hypotheses	acunirnmpt.0	$⊢ φ \to A \in V$
	acunirnmpt.1	$⊢ (φ \land j \in A) \to B \neq \emptyset$
	aciunf1lem.a	$⊢ \underline{Ⅎ} j A$
	aciunf1lem.1	$⊢ (φ \land j \in A) \to B \in W$
Assertion	aciunf1lem	$⊢ φ \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x)$

Proof

Step	Hyp	Ref	Expression
1		acunirnmpt.0	$⊢ φ \to A \in V$
2		acunirnmpt.1	$⊢ (φ \land j \in A) \to B \neq \emptyset$
3		aciunf1lem.a	$⊢ \underline{Ⅎ} j A$
4		aciunf1lem.1	$⊢ (φ \land j \in A) \to B \in W$
5		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} B$
6		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ g (x) / j ⦌ B$
7		eqid	$⊢ ⋃_{j \in A} B = ⋃_{j \in A} B$
8		csbeq1a	$⊢ j = g (x) \to B = ⦋ g (x) / j ⦌ B$
9	1 2 3 5 6 7 8 4	acunirnmpt2f	$⊢ φ \to \exists g (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)$
10		nfv	$⊢ Ⅎ x φ$
11		nfv	$⊢ Ⅎ x g : ⋃_{j \in A} B ⟶ A$
12		nfra1	$⊢ Ⅎ x \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B$
13	11 12	nfan	$⊢ Ⅎ x (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)$
14	10 13	nfan	$⊢ Ⅎ x (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B))$
15		nfv	$⊢ Ⅎ j φ$
16		nfcv	$⊢ \underline{Ⅎ} j g$
17	16 5 3	nff	$⊢ Ⅎ j g : ⋃_{j \in A} B ⟶ A$
18		nfcv	$⊢ \underline{Ⅎ} j x$
19	18 6	nfel	$⊢ Ⅎ j x \in ⦋ g (x) / j ⦌ B$
20	5 19	nfralw	$⊢ Ⅎ j \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B$
21	17 20	nfan	$⊢ Ⅎ j (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)$
22	15 21	nfan	$⊢ Ⅎ j (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B))$
23	18 5	nfel	$⊢ Ⅎ j x \in ⋃_{j \in A} B$
24	22 23	nfan	$⊢ Ⅎ j ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B)$
25		nfcv	$⊢ \underline{Ⅎ} j ⟨g (x), x⟩$
26		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times B)$
27	25 26	nfel	$⊢ Ⅎ j ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B)$
28		simplr	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)$
29	28	simpld	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to g : ⋃_{j \in A} B ⟶ A$
30	29	ad2antrr	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to g : ⋃_{j \in A} B ⟶ A$
31		simpllr	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to x \in ⋃_{j \in A} B$
32	30 31	ffvelcdmd	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to g (x) \in A$
33		fvex	$⊢ g (x) \in V$
34	33	snid	$⊢ g (x) \in \{g (x)\}$
35	34	a1i	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to g (x) \in \{g (x)\}$
36	28	simprd	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B$
37		simpr	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to x \in ⋃_{j \in A} B$
38		rsp	$⊢ \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B \to (x \in ⋃_{j \in A} B \to x \in ⦋ g (x) / j ⦌ B)$
39	36 37 38	sylc	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to x \in ⦋ g (x) / j ⦌ B$
40	39	ad2antrr	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to x \in ⦋ g (x) / j ⦌ B$
41	35 40	jca	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to (g (x) \in \{g (x)\} \land x \in ⦋ g (x) / j ⦌ B)$
42		opelxp	$⊢ ⟨g (x), x⟩ \in (\{g (x)\} \times ⦋ g (x) / j ⦌ B) \leftrightarrow (g (x) \in \{g (x)\} \land x \in ⦋ g (x) / j ⦌ B)$
43	41 42	sylibr	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to ⟨g (x), x⟩ \in (\{g (x)\} \times ⦋ g (x) / j ⦌ B)$
44		sneq	$⊢ k = g (x) \to \{k\} = \{g (x)\}$
45		csbeq1	$⊢ k = g (x) \to ⦋ k / j ⦌ B = ⦋ g (x) / j ⦌ B$
46	44 45	xpeq12d	$⊢ k = g (x) \to \{k\} \times ⦋ k / j ⦌ B = \{g (x)\} \times ⦋ g (x) / j ⦌ B$
47	46	eleq2d	$⊢ k = g (x) \to (⟨g (x), x⟩ \in (\{k\} \times ⦋ k / j ⦌ B) \leftrightarrow ⟨g (x), x⟩ \in (\{g (x)\} \times ⦋ g (x) / j ⦌ B))$
48	47	rspcev	$⊢ (g (x) \in A \land ⟨g (x), x⟩ \in (\{g (x)\} \times ⦋ g (x) / j ⦌ B)) \to \exists k \in A ⟨g (x), x⟩ \in (\{k\} \times ⦋ k / j ⦌ B)$
49	32 43 48	syl2anc	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to \exists k \in A ⟨g (x), x⟩ \in (\{k\} \times ⦋ k / j ⦌ B)$
50		eliun	$⊢ ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \in A ⟨g (x), x⟩ \in (\{j\} \times B)$
51		nfcv	$⊢ \underline{Ⅎ} k A$
52		nfv	$⊢ Ⅎ k ⟨g (x), x⟩ \in (\{j\} \times B)$
53		nfcv	$⊢ \underline{Ⅎ} j \{k\}$
54		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ k / j ⦌ B$
55	53 54	nfxp	$⊢ \underline{Ⅎ} j (\{k\} \times ⦋ k / j ⦌ B)$
56	25 55	nfel	$⊢ Ⅎ j ⟨g (x), x⟩ \in (\{k\} \times ⦋ k / j ⦌ B)$
57		sneq	$⊢ j = k \to \{j\} = \{k\}$
58		csbeq1a	$⊢ j = k \to B = ⦋ k / j ⦌ B$
59	57 58	xpeq12d	$⊢ j = k \to \{j\} \times B = \{k\} \times ⦋ k / j ⦌ B$
60	59	eleq2d	$⊢ j = k \to (⟨g (x), x⟩ \in (\{j\} \times B) \leftrightarrow ⟨g (x), x⟩ \in (\{k\} \times ⦋ k / j ⦌ B))$
61	3 51 52 56 60	cbvrexfw	$⊢ \exists j \in A ⟨g (x), x⟩ \in (\{j\} \times B) \leftrightarrow \exists k \in A ⟨g (x), x⟩ \in (\{k\} \times ⦋ k / j ⦌ B)$
62	50 61	bitri	$⊢ ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists k \in A ⟨g (x), x⟩ \in (\{k\} \times ⦋ k / j ⦌ B)$
63	49 62	sylibr	$⊢ ((((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \land j \in A) \land x \in B) \to ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B)$
64		eliun	$⊢ x \in ⋃_{j \in A} B \leftrightarrow \exists j \in A x \in B$
65	64	bilani	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to \exists j \in A x \in B$
66	24 27 63 65	r19.29af2	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B)$
67	66	ex	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to (x \in ⋃_{j \in A} B \to ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B))$
68	14 67	ralrimi	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to \forall x \in ⋃_{j \in A} B ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B)$
69		vex	$⊢ x \in V$
70	33 69	opth	$⊢ ⟨g (x), x⟩ = ⟨g (y), y⟩ \leftrightarrow (g (x) = g (y) \land x = y)$
71	70	simprbi	$⊢ ⟨g (x), x⟩ = ⟨g (y), y⟩ \to x = y$
72	71	rgen2w	$⊢ \forall x \in ⋃_{j \in A} B \forall y \in ⋃_{j \in A} B (⟨g (x), x⟩ = ⟨g (y), y⟩ \to x = y)$
73	72	a1i	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to \forall x \in ⋃_{j \in A} B \forall y \in ⋃_{j \in A} B (⟨g (x), x⟩ = ⟨g (y), y⟩ \to x = y)$
74	68 73	jca	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to (\forall x \in ⋃_{j \in A} B ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B \forall y \in ⋃_{j \in A} B (⟨g (x), x⟩ = ⟨g (y), y⟩ \to x = y))$
75		eqid	$⊢ (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩)$
76		fveq2	$⊢ x = y \to g (x) = g (y)$
77		id	$⊢ x = y \to x = y$
78	76 77	opeq12d	$⊢ x = y \to ⟨g (x), x⟩ = ⟨g (y), y⟩$
79	75 78	f1mpt	$⊢ (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \leftrightarrow (\forall x \in ⋃_{j \in A} B ⟨g (x), x⟩ \in ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B \forall y \in ⋃_{j \in A} B (⟨g (x), x⟩ = ⟨g (y), y⟩ \to x = y))$
80	74 79	sylibr	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B)$
81		opex	$⊢ ⟨g (x), x⟩ \in V$
82	75	fvmpt2	$⊢ (x \in ⋃_{j \in A} B \land ⟨g (x), x⟩ \in V) \to (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x) = ⟨g (x), x⟩$
83	81 82	mpan2	$⊢ x \in ⋃_{j \in A} B \to (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x) = ⟨g (x), x⟩$
84	37 83	syl	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x) = ⟨g (x), x⟩$
85	84	fveq2d	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = 2^{nd} (⟨g (x), x⟩)$
86	33 69	op2nd	$⊢ 2^{nd} (⟨g (x), x⟩) = x$
87	85 86	eqtrdi	$⊢ ((φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \land x \in ⋃_{j \in A} B) \to 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x$
88	87	ex	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to (x \in ⋃_{j \in A} B \to 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x)$
89	14 88	ralrimi	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to \forall x \in ⋃_{j \in A} B 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x$
90	80 89	jca	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x)$
91		nfcv	$⊢ \underline{Ⅎ} j k$
92	91 3	nfel	$⊢ Ⅎ j k \in A$
93	15 92	nfan	$⊢ Ⅎ j (φ \land k \in A)$
94		nfcv	$⊢ \underline{Ⅎ} j W$
95	54 94	nfel	$⊢ Ⅎ j ⦋ k / j ⦌ B \in W$
96	93 95	nfim	$⊢ Ⅎ j ((φ \land k \in A) \to ⦋ k / j ⦌ B \in W)$
97		eleq1w	$⊢ j = k \to (j \in A \leftrightarrow k \in A)$
98	97	anbi2d	$⊢ j = k \to ((φ \land j \in A) \leftrightarrow (φ \land k \in A))$
99	58	eleq1d	$⊢ j = k \to (B \in W \leftrightarrow ⦋ k / j ⦌ B \in W)$
100	98 99	imbi12d	$⊢ j = k \to (((φ \land j \in A) \to B \in W) \leftrightarrow ((φ \land k \in A) \to ⦋ k / j ⦌ B \in W))$
101	96 100 4	chvarfv	$⊢ (φ \land k \in A) \to ⦋ k / j ⦌ B \in W$
102	101	ralrimiva	$⊢ φ \to \forall k \in A ⦋ k / j ⦌ B \in W$
103		nfcv	$⊢ \underline{Ⅎ} k B$
104	3 51 103 54 58	cbviunf	$⊢ ⋃_{j \in A} B = ⋃_{k \in A} ⦋ k / j ⦌ B$
105		iunexg	$⊢ (A \in V \land \forall k \in A ⦋ k / j ⦌ B \in W) \to ⋃_{k \in A} ⦋ k / j ⦌ B \in V$
106	104 105	eqeltrid	$⊢ (A \in V \land \forall k \in A ⦋ k / j ⦌ B \in W) \to ⋃_{j \in A} B \in V$
107	1 102 106	syl2anc	$⊢ φ \to ⋃_{j \in A} B \in V$
108		mptexg	$⊢ ⋃_{j \in A} B \in V \to (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \in V$
109		f1eq1	$⊢ f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \to (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \leftrightarrow (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B))$
110		nfcv	$⊢ \underline{Ⅎ} x f$
111		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩)$
112	110 111	nfeq	$⊢ Ⅎ x f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩)$
113		fveq1	$⊢ f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \to f (x) = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)$
114	113	fveqeq2d	$⊢ f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \to (2^{nd} (f (x)) = x \leftrightarrow 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x)$
115	112 114	ralbid	$⊢ f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \to (\forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x \leftrightarrow \forall x \in ⋃_{j \in A} B 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x)$
116	109 115	anbi12d	$⊢ f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \to ((f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x) \leftrightarrow ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x))$
117	116	spcegv	$⊢ (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \in V \to (((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x) \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x))$
118	107 108 117	3syl	$⊢ φ \to (((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x) \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x))$
119	118	adantr	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to (((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} ((x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)) = x) \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x))$
120	90 119	mpd	$⊢ (φ \land (g : ⋃_{j \in A} B ⟶ A \land \forall x \in ⋃_{j \in A} B x \in ⦋ g (x) / j ⦌ B)) \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x)$
121	9 120	exlimddv	$⊢ φ \to \exists f (f : ⋃_{j \in A} B \underset{1-1}{⟶} ⋃_{j \in A} (\{j\} \times B) \land \forall x \in ⋃_{j \in A} B 2^{nd} (f (x)) = x)$

Metamath Proof Explorer

Theorem aciunf1lem

Proof