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 32672

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 5027	. . 3 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵
5		nfcsb1v 3923	. . 3 ⊢ Ⅎ𝑗⦋(𝑔‘𝑥) / 𝑗⦌𝐵
6		eqid 2737	. . 3 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵
7		csbeq1a 3913	. . 3 ⊢ (𝑗 = (𝑔‘𝑥) → 𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
8		aciunf1lem.1	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
9	1, 2, 3, 4, 5, 6, 7, 8	acunirnmpt2f 32671	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
10		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑥𝜑
11		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
12		nfra1 3284	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
13	11, 12	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
14	10, 13	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
15		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
16		nfcv 2905	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝑔
17	16, 4, 3	nff 6732	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
18		nfcv 2905	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝑥
19	18, 5	nfel 2920	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
20	4, 19	nfralw 3311	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
21	17, 20	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑗(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
22	15, 21	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
23	18, 4	nfel 2920	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
24	22, 23	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑗((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
25		nfcv 2905	. . . . . . . . . 10 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩
26		nfiu1 5027	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
27	25, 26	nfel 2920	. . . . . . . . 9 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
28		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
29	28	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
30	29	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
31		simpllr 776	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
32	30, 31	ffvelcdmd 7105	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ 𝐴)
33		fvex 6919	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑥) ∈ V
34	33	snid 4662	. . . . . . . . . . . . . 14 ⊢ (𝑔‘𝑥) ∈ {(𝑔‘𝑥)}
35	34	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ {(𝑔‘𝑥)})
36	28	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
37		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
38		rsp 3247	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵 → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
39	36, 37, 38	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
40	39	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
41	35, 40	jca 511	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
42		opelxp 5721	. . . . . . . . . . . 12 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵) ↔ ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
43	41, 42	sylibr 234	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
44		sneq 4636	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → {𝑘} = {(𝑔‘𝑥)})
45		csbeq1 3902	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → ⦋𝑘 / 𝑗⦌𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
46	44, 45	xpeq12d 5716	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑔‘𝑥) → ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) = ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
47	46	eleq2d 2827	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑔‘𝑥) → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)))
48	47	rspcev 3622	. . . . . . . . . . 11 ⊢ (((𝑔‘𝑥) ∈ 𝐴 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
49	32, 43, 48	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
50		eliun 4995	. . . . . . . . . . 11 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵))
51		nfcv 2905	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝐴
52		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵)
53		nfcv 2905	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗{𝑘}
54		nfcsb1v 3923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵
55	53, 54	nfxp 5718	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
56	25, 55	nfel 2920	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
57		sneq 4636	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → {𝑗} = {𝑘})
58		csbeq1a 3913	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑗⦌𝐵)
59	57, 58	xpeq12d 5716	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ({𝑗} × 𝐵) = ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
60	59	eleq2d 2827	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)))
61	3, 51, 52, 56, 60	cbvrexfw 3305	. . . . . . . . . . 11 ⊢ (∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
62	50, 61	bitri 275	. . . . . . . . . 10 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
63	49, 62	sylibr 234	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
64		eliun 4995	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
65	64	biimpi 216	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
66	65	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
67	24, 27, 63, 66	r19.29af2 3267	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
68	67	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
69	14, 68	ralrimi 3257	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
70		vex 3484	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
71	33, 70	opth 5481	. . . . . . . . 9 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ ↔ ((𝑔‘𝑥) = (𝑔‘𝑦) ∧ 𝑥 = 𝑦))
72	71	simprbi 496	. . . . . . . 8 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
73	72	rgen2w 3066	. . . . . . 7 ⊢ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
74	73	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦))
75	69, 74	jca 511	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
76		eqid 2737	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
77		fveq2 6906	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦))
78		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
79	77, 78	opeq12d 4881	. . . . . 6 ⊢ (𝑥 = 𝑦 → ⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩)
80	76, 79	f1mpt 7281	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
81	75, 80	sylibr 234	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
82		opex 5469	. . . . . . . . . 10 ⊢ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V
83	76	fvmpt2 7027	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
84	82, 83	mpan2 691	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
85	37, 84	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
86	85	fveq2d 6910	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩))
87	33, 70	op2nd 8023	. . . . . . 7 ⊢ (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩) = 𝑥
88	86, 87	eqtrdi 2793	. . . . . 6 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
89	88	ex 412	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
90	14, 89	ralrimi 3257	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
91	81, 90	jca 511	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
92		nfcv 2905	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝑘
93	92, 3	nfel 2920	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑘 ∈ 𝐴
94	15, 93	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ 𝐴)
95		nfcv 2905	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑊
96	54, 95	nfel 2920	. . . . . . . . 9 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊
97	94, 96	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
98		eleq1w 2824	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
99	98	anbi2d 630	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝐴) ↔ (𝜑 ∧ 𝑘 ∈ 𝐴)))
100	58	eleq1d 2826	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐵 ∈ 𝑊 ↔ ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊))
101	99, 100	imbi12d 344	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)))
102	97, 101, 8	chvarfv 2240	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
103	102	ralrimiva 3146	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
104		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑘𝐵
105	3, 51, 104, 54, 58	cbviunf 32568	. . . . . . 7 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵
106		iunexg 7988	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ V)
107	105, 106	eqeltrid 2845	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
108	1, 103, 107	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
109		mptexg 7241	. . . . 5 ⊢ (∪ 𝑗 ∈ 𝐴 𝐵 ∈ V → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V)
110		f1eq1 6799	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
111		nfcv 2905	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑓
112		nfmpt1 5250	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
113	111, 112	nfeq 2919	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
114		fveq1 6905	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓‘𝑥) = ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥))
115	114	fveqeq2d 6914	. . . . . . . 8 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
116	113, 115	ralbid 3273	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
117	110, 116	anbi12d 632	. . . . . 6 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥) ↔ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)))
118	117	spcegv 3597	. . . . 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 480	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥)))
121	91, 120	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))
122	9, 121	exlimddv 1935	1 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 Ⅎwnfc 2890 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ⦋csb 3899 ∅c0 4333 {csn 4626 ⟨cop 4632 ∪ ciun 4991 ↦ cmpt 5225 × cxp 5683 ⟶wf 6557 –1-1→wf1 6558 ‘cfv 6561 2^nd c2nd 8013

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-reg 9632 ax-inf2 9681 ax-ac2 10503

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-om 7888 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-en 8986 df-r1 9804 df-rank 9805 df-card 9979 df-ac 10156

This theorem is referenced by: aciunf1 32673

W3C validator