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 33007

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 4992	. . 3 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵
5		nfcsb1v 3877	. . 3 ⊢ Ⅎ𝑗⦋(𝑔‘𝑥) / 𝑗⦌𝐵
6		eqid 2763	. . 3 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵
7		csbeq1a 3867	. . 3 ⊢ (𝑗 = (𝑔‘𝑥) → 𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
8		aciunf1lem.1	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
9	1, 2, 3, 4, 5, 6, 7, 8	acunirnmpt2f 33006	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
10		nfv 1944	. . . . . . . 8 ⊢ Ⅎ𝑥𝜑
11		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
12		nfra1 3289	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
13	11, 12	nfan 1929	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
14	10, 13	nfan 1929	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
15		nfv 1944	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
16		nfcv 2925	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝑔
17	16, 4, 3	nff 6701	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
18		nfcv 2925	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝑥
19	18, 5	nfel 2939	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
20	4, 19	nfralw 3312	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
21	17, 20	nfan 1929	. . . . . . . . . . 11 ⊢ Ⅎ𝑗(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
22	15, 21	nfan 1929	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
23	18, 4	nfel 2939	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
24	22, 23	nfan 1929	. . . . . . . . 9 ⊢ Ⅎ𝑗((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
25		nfcv 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩
26		nfiu1 4992	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
27	25, 26	nfel 2939	. . . . . . . . 9 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
28		simplr 780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
29	28	simpld 499	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
30	29	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
31		simpllr 787	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
32	30, 31	ffvelcdmd 7080	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ 𝐴)
33		fvex 6894	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑥) ∈ V
34	33	snid 4628	. . . . . . . . . . . . . 14 ⊢ (𝑔‘𝑥) ∈ {(𝑔‘𝑥)}
35	34	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ {(𝑔‘𝑥)})
36	28	simprd 500	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
37		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
38		rsp 3253	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵 → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
39	36, 37, 38	sylc 66	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
40	39	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
41	35, 40	jca 520	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
42		opelxp 5697	. . . . . . . . . . . 12 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵) ↔ ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
43	41, 42	sylibr 237	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
44		sneq 4599	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → {𝑘} = {(𝑔‘𝑥)})
45		csbeq1 3856	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → ⦋𝑘 / 𝑗⦌𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
46	44, 45	xpeq12d 5692	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑔‘𝑥) → ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) = ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
47	46	eleq2d 2849	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑔‘𝑥) → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)))
48	47	rspcev 3581	. . . . . . . . . . 11 ⊢ (((𝑔‘𝑥) ∈ 𝐴 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
49	32, 43, 48	syl2anc 595	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
50		eliun 4960	. . . . . . . . . . 11 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵))
51		nfcv 2925	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝐴
52		nfv 1944	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵)
53		nfcv 2925	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗{𝑘}
54		nfcsb1v 3877	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵
55	53, 54	nfxp 5694	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
56	25, 55	nfel 2939	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
57		sneq 4599	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → {𝑗} = {𝑘})
58		csbeq1a 3867	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑗⦌𝐵)
59	57, 58	xpeq12d 5692	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ({𝑗} × 𝐵) = ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
60	59	eleq2d 2849	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)))
61	3, 51, 52, 56, 60	cbvrexfw 3306	. . . . . . . . . . 11 ⊢ (∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
62	50, 61	bitri 278	. . . . . . . . . 10 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
63	49, 62	sylibr 237	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
64		eliun 4960	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
65	64	bilani 509	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
66	24, 27, 63, 65	r19.29af2 3273	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
67	66	ex 417	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
68	14, 67	ralrimi 3263	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
69		vex 3459	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
70	33, 69	opth 5458	. . . . . . . . 9 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ ↔ ((𝑔‘𝑥) = (𝑔‘𝑦) ∧ 𝑥 = 𝑦))
71	70	simprbi 502	. . . . . . . 8 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
72	71	rgen2w 3084	. . . . . . 7 ⊢ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
73	72	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦))
74	68, 73	jca 520	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
75		eqid 2763	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
76		fveq2 6881	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦))
77		id 23	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
78	76, 77	opeq12d 4846	. . . . . 6 ⊢ (𝑥 = 𝑦 → ⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩)
79	75, 78	f1mpt 7259	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
80	74, 79	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
81		opex 5445	. . . . . . . . . 10 ⊢ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V
82	75	fvmpt2 7001	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
83	81, 82	mpan2 703	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
84	37, 83	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
85	84	fveq2d 6885	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩))
86	33, 69	op2nd 7991	. . . . . . 7 ⊢ (2^nd ‘⟨(𝑔‘𝑥), 𝑥⟩) = 𝑥
87	85, 86	eqtrdi 2814	. . . . . 6 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
88	87	ex 417	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
89	14, 88	ralrimi 3263	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
90	80, 89	jca 520	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
91		nfcv 2925	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝑘
92	91, 3	nfel 2939	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑘 ∈ 𝐴
93	15, 92	nfan 1929	. . . . . . . . 9 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ 𝐴)
94		nfcv 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑊
95	54, 94	nfel 2939	. . . . . . . . 9 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊
96	93, 95	nfim 1926	. . . . . . . 8 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
97		eleq1w 2846	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
98	97	anbi2d 641	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝐴) ↔ (𝜑 ∧ 𝑘 ∈ 𝐴)))
99	58	eleq1d 2848	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐵 ∈ 𝑊 ↔ ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊))
100	98, 99	imbi12d 347	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)))
101	96, 100, 8	chvarfv 2276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
102	101	ralrimiva 3157	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
103		nfcv 2925	. . . . . . . 8 ⊢ Ⅎ𝑘𝐵
104	3, 51, 103, 54, 58	cbviunf 32900	. . . . . . 7 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵
105		iunexg 7956	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ V)
106	104, 105	eqeltrid 2867	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
107	1, 102, 106	syl2anc 595	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
108		mptexg 7219	. . . . 5 ⊢ (∪ 𝑗 ∈ 𝐴 𝐵 ∈ V → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V)
109		f1eq1 6769	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
110		nfcv 2925	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑓
111		nfmpt1 5210	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
112	110, 111	nfeq 2938	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
113		fveq1 6880	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓‘𝑥) = ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥))
114	113	fveqeq2d 6889	. . . . . . . 8 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ (2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
115	112, 114	ralbid 3278	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥 ↔ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
116	109, 115	anbi12d 643	. . . . . 6 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥) ↔ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)))
117	116	spcegv 3556	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥)))
118	107, 108, 117	3syl 19	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥)))
119	118	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥)))
120	90, 119	mpd 16	. 2 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))
121	9, 120	exlimddv 1965	1 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2^nd ‘(𝑓‘𝑥)) = 𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1570 ∃wex 1809 ∈ wcel 2143 Ⅎwnfc 2910 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 Vcvv 3455 ⦋csb 3853 ∅c0 4286 {csn 4589 ⟨cop 4595 ∪ ciun 4956 ↦ cmpt 5192 × cxp 5659 ⟶wf 6532 –1-1→wf1 6533 ‘cfv 6536 2^nd c2nd 7981

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-reg 9550 ax-inf2 9606 ax-ac2 10442

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-om 7859 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-en 8940 df-r1 9732 df-rank 9733 df-card 9921 df-ac 10096

This theorem is referenced by: aciunf1 33008

W3C validator