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 30901

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 4955	. . 3 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵
5		nfcsb1v 3853	. . 3 ⊢ Ⅎ𝑗⦋(𝑔‘𝑥) / 𝑗⦌𝐵
6		eqid 2738	. . 3 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵
7		csbeq1a 3842	. . 3 ⊢ (𝑗 = (𝑔‘𝑥) → 𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
8		aciunf1lem.1	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
9	1, 2, 3, 4, 5, 6, 7, 8	acunirnmpt2f 30900	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
10		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑥𝜑
11		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
12		nfra1 3142	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
13	11, 12	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
14	10, 13	nfan 1903	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
15		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
16		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝑔
17	16, 4, 3	nff 6580	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
18		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝑥
19	18, 5	nfel 2920	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
20	4, 19	nfralw 3149	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
21	17, 20	nfan 1903	. . . . . . . . . . 11 ⊢ Ⅎ𝑗(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
22	15, 21	nfan 1903	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
23	18, 4	nfel 2920	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
24	22, 23	nfan 1903	. . . . . . . . 9 ⊢ Ⅎ𝑗((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
25		nfcv 2906	. . . . . . . . . 10 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩
26		nfiu1 4955	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
27	25, 26	nfel 2920	. . . . . . . . 9 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
28		simplr 765	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
29	28	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
30	29	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
31		simpllr 772	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
32	30, 31	ffvelrnd 6944	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ 𝐴)
33		fvex 6769	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑥) ∈ V
34	33	snid 4594	. . . . . . . . . . . . . 14 ⊢ (𝑔‘𝑥) ∈ {(𝑔‘𝑥)}
35	34	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ {(𝑔‘𝑥)})
36	28	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
37		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
38		rsp 3129	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵 → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
39	36, 37, 38	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
40	39	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
41	35, 40	jca 511	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
42		opelxp 5616	. . . . . . . . . . . 12 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵) ↔ ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
43	41, 42	sylibr 233	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
44		sneq 4568	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → {𝑘} = {(𝑔‘𝑥)})
45		csbeq1 3831	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → ⦋𝑘 / 𝑗⦌𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
46	44, 45	xpeq12d 5611	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑔‘𝑥) → ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) = ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
47	46	eleq2d 2824	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑔‘𝑥) → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)))
48	47	rspcev 3552	. . . . . . . . . . 11 ⊢ (((𝑔‘𝑥) ∈ 𝐴 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
49	32, 43, 48	syl2anc 583	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
50		eliun 4925	. . . . . . . . . . 11 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵))
51		nfcv 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝐴
52		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵)
53		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗{𝑘}
54		nfcsb1v 3853	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵
55	53, 54	nfxp 5613	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
56	25, 55	nfel 2920	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
57		sneq 4568	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → {𝑗} = {𝑘})
58		csbeq1a 3842	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑗⦌𝐵)
59	57, 58	xpeq12d 5611	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ({𝑗} × 𝐵) = ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
60	59	eleq2d 2824	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)))
61	3, 51, 52, 56, 60	cbvrexfw 3360	. . . . . . . . . . 11 ⊢ (∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
62	50, 61	bitri 274	. . . . . . . . . 10 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
63	49, 62	sylibr 233	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
64		eliun 4925	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
65	64	biimpi 215	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
66	65	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
67	24, 27, 63, 66	r19.29af2 3258	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
68	67	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
69	14, 68	ralrimi 3139	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
70		vex 3426	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
71	33, 70	opth 5385	. . . . . . . . 9 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ ↔ ((𝑔‘𝑥) = (𝑔‘𝑦) ∧ 𝑥 = 𝑦))
72	71	simprbi 496	. . . . . . . 8 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
73	72	rgen2w 3076	. . . . . . 7 ⊢ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
74	73	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦))
75	69, 74	jca 511	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
76		eqid 2738	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
77		fveq2 6756	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦))
78		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
79	77, 78	opeq12d 4809	. . . . . 6 ⊢ (𝑥 = 𝑦 → ⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩)
80	76, 79	f1mpt 7115	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
81	75, 80	sylibr 233	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
82		opex 5373	. . . . . . . . . 10 ⊢ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V
83	76	fvmpt2 6868	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
84	82, 83	mpan2 687	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
85	37, 84	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
86	85	fveq2d 6760	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩))
87	33, 70	op2nd 7813	. . . . . . 7 ⊢ (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩) = 𝑥
88	86, 87	eqtrdi 2795	. . . . . 6 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
89	88	ex 412	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
90	14, 89	ralrimi 3139	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
91	81, 90	jca 511	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
92		nfcv 2906	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝑘
93	92, 3	nfel 2920	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑘 ∈ 𝐴
94	15, 93	nfan 1903	. . . . . . . . 9 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ 𝐴)
95		nfcv 2906	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑊
96	54, 95	nfel 2920	. . . . . . . . 9 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊
97	94, 96	nfim 1900	. . . . . . . 8 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
98		eleq1w 2821	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
99	98	anbi2d 628	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝐴) ↔ (𝜑 ∧ 𝑘 ∈ 𝐴)))
100	58	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐵 ∈ 𝑊 ↔ ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊))
101	99, 100	imbi12d 344	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)))
102	97, 101, 8	chvarfv 2236	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
103	102	ralrimiva 3107	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
104		nfcv 2906	. . . . . . . 8 ⊢ Ⅎ𝑘𝐵
105	3, 51, 104, 54, 58	cbviunf 30796	. . . . . . 7 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵
106		iunexg 7779	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ V)
107	105, 106	eqeltrid 2843	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
108	1, 103, 107	syl2anc 583	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
109		mptexg 7079	. . . . 5 ⊢ (∪ 𝑗 ∈ 𝐴 𝐵 ∈ V → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V)
110		f1eq1 6649	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
111		nfcv 2906	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑓
112		nfmpt1 5178	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
113	111, 112	nfeq 2919	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
114		fveq1 6755	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓‘𝑥) = ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥))
115	114	fveqeq2d 6764	. . . . . . . 8 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
116	113, 115	ralbid 3158	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
117	110, 116	anbi12d 630	. . . . . 6 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥) ↔ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)))
118	117	spcegv 3526	. . . . 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 1939	1 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∃wex 1783 ∈ wcel 2108 Ⅎwnfc 2886 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ⦋csb 3828 ∅c0 4253 {csn 4558 ⟨cop 4564 ∪ ciun 4921 ↦ cmpt 5153 × cxp 5578 ⟶wf 6414 –1-1→wf1 6415 ‘cfv 6418 2^nd c2nd 7803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-reg 9281 ax-inf2 9329 ax-ac2 10150

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-en 8692 df-r1 9453 df-rank 9454 df-card 9628 df-ac 9803

This theorem is referenced by: aciunf1 30902

W3C validator