aciunf1lem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aciunf1lem		Structured version Visualization version GIF version

Theorem aciunf1lem 30691

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

**Hypotheses**
Ref	Expression
acunirnmpt.0	⊢ (𝜑 → 𝐴 ∈ 𝑉)
acunirnmpt.1	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)
aciunf1lem.a	⊢ Ⅎ𝑗𝐴
aciunf1lem.1	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)

**Assertion**
Ref	Expression
aciunf1lem	⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))

Distinct variable groups: 𝑓,𝑗,𝑥 𝐴,𝑓,𝑥 𝐵,𝑓,𝑥 𝑥,𝑗,𝜑 𝑗,𝑊 Allowed substitution hints: 𝜑(𝑓) 𝐴(𝑗) 𝐵(𝑗) 𝑉(𝑥,𝑓,𝑗) 𝑊(𝑥,𝑓)

Proof of Theorem aciunf1lem Dummy variables 𝑘 𝑦 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		acunirnmpt.0	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		acunirnmpt.1	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅)
3		aciunf1lem.a	. . 3 ⊢ Ⅎ𝑗𝐴
4		nfiu1 4928	. . 3 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵
5		nfcsb1v 3827	. . 3 ⊢ Ⅎ𝑗⦋(𝑔‘𝑥) / 𝑗⦌𝐵
6		eqid 2734	. . 3 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵
7		csbeq1a 3816	. . 3 ⊢ (𝑗 = (𝑔‘𝑥) → 𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
8		aciunf1lem.1	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
9	1, 2, 3, 4, 5, 6, 7, 8	acunirnmpt2f 30690	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
10		nfv 1922	. . . . . . . 8 ⊢ Ⅎ𝑥𝜑
11		nfv 1922	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
12		nfra1 3133	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
13	11, 12	nfan 1907	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
14	10, 13	nfan 1907	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
15		nfv 1922	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
16		nfcv 2900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝑔
17	16, 4, 3	nff 6530	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
18		nfcv 2900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝑥
19	18, 5	nfel 2914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
20	4, 19	nfralw 3140	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
21	17, 20	nfan 1907	. . . . . . . . . . 11 ⊢ Ⅎ𝑗(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
22	15, 21	nfan 1907	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
23	18, 4	nfel 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
24	22, 23	nfan 1907	. . . . . . . . 9 ⊢ Ⅎ𝑗((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
25		nfcv 2900	. . . . . . . . . 10 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩
26		nfiu1 4928	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
27	25, 26	nfel 2914	. . . . . . . . 9 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
28		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
29	28	simpld 498	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
30	29	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
31		simpllr 776	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
32	30, 31	ffvelrnd 6894	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ 𝐴)
33		fvex 6719	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑥) ∈ V
34	33	snid 4567	. . . . . . . . . . . . . 14 ⊢ (𝑔‘𝑥) ∈ {(𝑔‘𝑥)}
35	34	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ {(𝑔‘𝑥)})
36	28	simprd 499	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
37		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
38		rsp 3120	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵 → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
39	36, 37, 38	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
40	39	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
41	35, 40	jca 515	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
42		opelxp 5576	. . . . . . . . . . . 12 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵) ↔ ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
43	41, 42	sylibr 237	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
44		sneq 4541	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → {𝑘} = {(𝑔‘𝑥)})
45		csbeq1 3805	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → ⦋𝑘 / 𝑗⦌𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
46	44, 45	xpeq12d 5571	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑔‘𝑥) → ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) = ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
47	46	eleq2d 2819	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑔‘𝑥) → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)))
48	47	rspcev 3530	. . . . . . . . . . 11 ⊢ (((𝑔‘𝑥) ∈ 𝐴 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
49	32, 43, 48	syl2anc 587	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
50		eliun 4898	. . . . . . . . . . 11 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵))
51		nfcv 2900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝐴
52		nfv 1922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵)
53		nfcv 2900	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗{𝑘}
54		nfcsb1v 3827	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵
55	53, 54	nfxp 5573	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
56	25, 55	nfel 2914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
57		sneq 4541	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → {𝑗} = {𝑘})
58		csbeq1a 3816	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑗⦌𝐵)
59	57, 58	xpeq12d 5571	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ({𝑗} × 𝐵) = ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
60	59	eleq2d 2819	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)))
61	3, 51, 52, 56, 60	cbvrexfw 3339	. . . . . . . . . . 11 ⊢ (∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
62	50, 61	bitri 278	. . . . . . . . . 10 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
63	49, 62	sylibr 237	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
64		eliun 4898	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
65	64	biimpi 219	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
66	65	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
67	24, 27, 63, 66	r19.29af2 3241	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
68	67	ex 416	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
69	14, 68	ralrimi 3130	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
70		vex 3405	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
71	33, 70	opth 5349	. . . . . . . . 9 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ ↔ ((𝑔‘𝑥) = (𝑔‘𝑦) ∧ 𝑥 = 𝑦))
72	71	simprbi 500	. . . . . . . 8 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
73	72	rgen2w 3067	. . . . . . 7 ⊢ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
74	73	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦))
75	69, 74	jca 515	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
76		eqid 2734	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
77		fveq2 6706	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦))
78		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
79	77, 78	opeq12d 4782	. . . . . 6 ⊢ (𝑥 = 𝑦 → ⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩)
80	76, 79	f1mpt 7062	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
81	75, 80	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
82		opex 5337	. . . . . . . . . 10 ⊢ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V
83	76	fvmpt2 6818	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
84	82, 83	mpan2 691	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
85	37, 84	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
86	85	fveq2d 6710	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩))
87	33, 70	op2nd 7759	. . . . . . 7 ⊢ (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩) = 𝑥
88	86, 87	eqtrdi 2790	. . . . . 6 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
89	88	ex 416	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
90	14, 89	ralrimi 3130	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
91	81, 90	jca 515	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
92		nfcv 2900	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝑘
93	92, 3	nfel 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑘 ∈ 𝐴
94	15, 93	nfan 1907	. . . . . . . . 9 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ 𝐴)
95		nfcv 2900	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑊
96	54, 95	nfel 2914	. . . . . . . . 9 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊
97	94, 96	nfim 1904	. . . . . . . 8 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
98		eleq1w 2816	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
99	98	anbi2d 632	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝐴) ↔ (𝜑 ∧ 𝑘 ∈ 𝐴)))
100	58	eleq1d 2818	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐵 ∈ 𝑊 ↔ ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊))
101	99, 100	imbi12d 348	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)))
102	97, 101, 8	chvarfv 2238	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
103	102	ralrimiva 3098	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
104		nfcv 2900	. . . . . . . 8 ⊢ Ⅎ𝑘𝐵
105	3, 51, 104, 54, 58	cbviunf 30586	. . . . . . 7 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵
106		iunexg 7725	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ V)
107	105, 106	eqeltrid 2838	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
108	1, 103, 107	syl2anc 587	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
109		mptexg 7026	. . . . 5 ⊢ (∪ 𝑗 ∈ 𝐴 𝐵 ∈ V → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V)
110		f1eq1 6599	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
111		nfcv 2900	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑓
112		nfmpt1 5142	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
113	111, 112	nfeq 2913	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
114		fveq1 6705	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓‘𝑥) = ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥))
115	114	fveqeq2d 6714	. . . . . . . 8 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
116	113, 115	ralbid 3147	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
117	110, 116	anbi12d 634	. . . . . 6 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥) ↔ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)))
118	117	spcegv 3505	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥)))
119	108, 109, 118	3syl 18	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥)))
120	119	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥)))
121	91, 120	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))
122	9, 121	exlimddv 1943	1 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∃wex 1787 ∈ wcel 2110 Ⅎwnfc 2880 ≠ wne 2935 ∀wral 3054 ∃wrex 3055 Vcvv 3401 ⦋csb 3802 ∅c0 4227 {csn 4531 ⟨cop 4537 ∪ ciun 4894 ↦ cmpt 5124 × cxp 5538 ⟶wf 6365 –1-1→wf1 6366 ‘cfv 6369 2^nd c2nd 7749

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-reg 9197 ax-inf2 9245 ax-ac2 10060

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-iin 4897 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-se 5499 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-isom 6378 df-riota 7159 df-om 7634 df-2nd 7751 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-en 8616 df-r1 9363 df-rank 9364 df-card 9538 df-ac 9713

This theorem is referenced by: aciunf1 30692

W3C validator