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	biimpi	$⊢ x \in ⋃_{j \in A} B \to \exists j \in A x \in B$
66	65	adantl	$⊢ ((φ \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$
67	24 27 63 66	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)$
68	67	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))$
69	14 68	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)$
70		vex	$⊢ x \in V$
71	33 70	opth	$⊢ ⟨g (x), x⟩ = ⟨g (y), y⟩ \leftrightarrow (g (x) = g (y) \land x = y)$
72	71	simprbi	$⊢ ⟨g (x), x⟩ = ⟨g (y), y⟩ \to x = y$
73	72	rgen2w	$⊢ \forall x \in ⋃_{j \in A} B \forall y \in ⋃_{j \in A} B (⟨g (x), x⟩ = ⟨g (y), y⟩ \to x = y)$
74	73	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)$
75	69 74	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))$
76		eqid	$⊢ (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩)$
77		fveq2	$⊢ x = y \to g (x) = g (y)$
78		id	$⊢ x = y \to x = y$
79	77 78	opeq12d	$⊢ x = y \to ⟨g (x), x⟩ = ⟨g (y), y⟩$
80	76 79	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))$
81	75 80	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)$
82		opex	$⊢ ⟨g (x), x⟩ \in V$
83	76	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⟩$
84	82 83	mpan2	$⊢ x \in ⋃_{j \in A} B \to (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x) = ⟨g (x), x⟩$
85	37 84	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⟩$
86	85	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⟩)$
87	33 70	op2nd	$⊢ 2^{nd} (⟨g (x), x⟩) = x$
88	86 87	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$
89	88	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)$
90	14 89	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$
91	81 90	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)$
92		nfcv	$⊢ \underline{Ⅎ} j k$
93	92 3	nfel	$⊢ Ⅎ j k \in A$
94	15 93	nfan	$⊢ Ⅎ j (φ \land k \in A)$
95		nfcv	$⊢ \underline{Ⅎ} j W$
96	54 95	nfel	$⊢ Ⅎ j ⦋ k / j ⦌ B \in W$
97	94 96	nfim	$⊢ Ⅎ j ((φ \land k \in A) \to ⦋ k / j ⦌ B \in W)$
98		eleq1w	$⊢ j = k \to (j \in A \leftrightarrow k \in A)$
99	98	anbi2d	$⊢ j = k \to ((φ \land j \in A) \leftrightarrow (φ \land k \in A))$
100	58	eleq1d	$⊢ j = k \to (B \in W \leftrightarrow ⦋ k / j ⦌ B \in W)$
101	99 100	imbi12d	$⊢ j = k \to (((φ \land j \in A) \to B \in W) \leftrightarrow ((φ \land k \in A) \to ⦋ k / j ⦌ B \in W))$
102	97 101 4	chvarfv	$⊢ (φ \land k \in A) \to ⦋ k / j ⦌ B \in W$
103	102	ralrimiva	$⊢ φ \to \forall k \in A ⦋ k / j ⦌ B \in W$
104		nfcv	$⊢ \underline{Ⅎ} k B$
105	3 51 104 54 58	cbviunf	$⊢ ⋃_{j \in A} B = ⋃_{k \in A} ⦋ k / j ⦌ B$
106		iunexg	$⊢ (A \in V \land \forall k \in A ⦋ k / j ⦌ B \in W) \to ⋃_{k \in A} ⦋ k / j ⦌ B \in V$
107	105 106	eqeltrid	$⊢ (A \in V \land \forall k \in A ⦋ k / j ⦌ B \in W) \to ⋃_{j \in A} B \in V$
108	1 103 107	syl2anc	$⊢ φ \to ⋃_{j \in A} B \in V$
109		mptexg	$⊢ ⋃_{j \in A} B \in V \to (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \in V$
110		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))$
111		nfcv	$⊢ \underline{Ⅎ} x f$
112		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩)$
113	111 112	nfeq	$⊢ Ⅎ x f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩)$
114		fveq1	$⊢ f = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) \to f (x) = (x \in ⋃_{j \in A} B ⟼ ⟨g (x), x⟩) (x)$
115	114	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)$
116	113 115	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)$
117	110 116	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))$
118	117	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))$
119	108 109 118	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))$
120	119	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))$
121	91 120	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)$
122	9 121	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