Theorem aciunf1lem 32593

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→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥))

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 4994	. . 3 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵
5		nfcsb1v 3889	. . 3 ⊢ Ⅎ𝑗⦋(𝑔‘𝑥) / 𝑗⦌𝐵
6		eqid 2730	. . 3 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵
7		csbeq1a 3879	. . 3 ⊢ (𝑗 = (𝑔‘𝑥) → 𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
8		aciunf1lem.1	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
9	1, 2, 3, 4, 5, 6, 7, 8	acunirnmpt2f 32592	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
10		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑥𝜑
11		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
12		nfra1 3262	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
13	11, 12	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
14	10, 13	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
15		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝜑
16		nfcv 2892	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝑔
17	16, 4, 3	nff 6687	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴
18		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝑥
19	18, 5	nfel 2907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
20	4, 19	nfralw 3287	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵
21	17, 20	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑗(𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
22	15, 21	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
23	18, 4	nfel 2907	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
24	22, 23	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑗((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
25		nfcv 2892	. . . . . . . . . 10 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩
26		nfiu1 4994	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
27	25, 26	nfel 2907	. . . . . . . . 9 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
28		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
29	28	simpld 494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
30	29	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴)
31		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
32	30, 31	ffvelcdmd 7060	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ 𝐴)
33		fvex 6874	. . . . . . . . . . . . . . 15 ⊢ (𝑔‘𝑥) ∈ V
34	33	snid 4629	. . . . . . . . . . . . . 14 ⊢ (𝑔‘𝑥) ∈ {(𝑔‘𝑥)}
35	34	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → (𝑔‘𝑥) ∈ {(𝑔‘𝑥)})
36	28	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
37		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
38		rsp 3226	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵 → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
39	36, 37, 38	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
40	39	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
41	35, 40	jca 511	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
42		opelxp 5677	. . . . . . . . . . . 12 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵) ↔ ((𝑔‘𝑥) ∈ {(𝑔‘𝑥)} ∧ 𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
43	41, 42	sylibr 234	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
44		sneq 4602	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → {𝑘} = {(𝑔‘𝑥)})
45		csbeq1 3868	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑔‘𝑥) → ⦋𝑘 / 𝑗⦌𝐵 = ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)
46	44, 45	xpeq12d 5672	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑔‘𝑥) → ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) = ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵))
47	46	eleq2d 2815	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑔‘𝑥) → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)))
48	47	rspcev 3591	. . . . . . . . . . 11 ⊢ (((𝑔‘𝑥) ∈ 𝐴 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({(𝑔‘𝑥)} × ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
49	32, 43, 48	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
50		eliun 4962	. . . . . . . . . . 11 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵))
51		nfcv 2892	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘𝐴
52		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵)
53		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗{𝑘}
54		nfcsb1v 3889	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵
55	53, 54	nfxp 5674	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
56	25, 55	nfel 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)
57		sneq 4602	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → {𝑗} = {𝑘})
58		csbeq1a 3879	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑗⦌𝐵)
59	57, 58	xpeq12d 5672	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑘 → ({𝑗} × 𝐵) = ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
60	59	eleq2d 2815	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵)))
61	3, 51, 52, 56, 60	cbvrexfw 3281	. . . . . . . . . . 11 ⊢ (∃𝑗 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
62	50, 61	bitri 275	. . . . . . . . . 10 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐴 ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ({𝑘} × ⦋𝑘 / 𝑗⦌𝐵))
63	49, 62	sylibr 234	. . . . . . . . 9 ⊢ (((((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
64		eliun 4962	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
65	64	biimpi 216	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
66	65	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)
67	24, 27, 63, 66	r19.29af2 3246	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
68	67	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
69	14, 68	ralrimi 3236	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
70		vex 3454	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
71	33, 70	opth 5439	. . . . . . . . 9 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ ↔ ((𝑔‘𝑥) = (𝑔‘𝑦) ∧ 𝑥 = 𝑦))
72	71	simprbi 496	. . . . . . . 8 ⊢ (⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
73	72	rgen2w 3050	. . . . . . 7 ⊢ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
74	73	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦))
75	69, 74	jca 511	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
76		eqid 2730	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
77		fveq2 6861	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦))
78		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
79	77, 78	opeq12d 4848	. . . . . 6 ⊢ (𝑥 = 𝑦 → ⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩)
80	76, 79	f1mpt 7239	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵⟨(𝑔‘𝑥), 𝑥⟩ ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵∀𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(⟨(𝑔‘𝑥), 𝑥⟩ = ⟨(𝑔‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)))
81	75, 80	sylibr 234	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
82		opex 5427	. . . . . . . . . 10 ⊢ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V
83	76	fvmpt2 6982	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ⟨(𝑔‘𝑥), 𝑥⟩ ∈ V) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
84	82, 83	mpan2 691	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
85	37, 84	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥) = ⟨(𝑔‘𝑥), 𝑥⟩)
86	85	fveq2d 6865	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = (2nd ‘⟨(𝑔‘𝑥), 𝑥⟩))
87	33, 70	op2nd 7980	. . . . . . 7 ⊢ (2nd ‘⟨(𝑔‘𝑥), 𝑥⟩) = 𝑥
88	86, 87	eqtrdi 2781	. . . . . 6 ⊢ (((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
89	88	ex 412	. . . . 5 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → (2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
90	14, 89	ralrimi 3236	. . . 4 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)
91	81, 90	jca 511	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
92		nfcv 2892	. . . . . . . . . . 11 ⊢ Ⅎ𝑗𝑘
93	92, 3	nfel 2907	. . . . . . . . . 10 ⊢ Ⅎ𝑗 𝑘 ∈ 𝐴
94	15, 93	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ 𝐴)
95		nfcv 2892	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑊
96	54, 95	nfel 2907	. . . . . . . . 9 ⊢ Ⅎ𝑗⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊
97	94, 96	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
98		eleq1w 2812	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
99	98	anbi2d 630	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝐴) ↔ (𝜑 ∧ 𝑘 ∈ 𝐴)))
100	58	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → (𝐵 ∈ 𝑊 ↔ ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊))
101	99, 100	imbi12d 344	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)))
102	97, 101, 8	chvarfv 2241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
103	102	ralrimiva 3126	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊)
104		nfcv 2892	. . . . . . . 8 ⊢ Ⅎ𝑘𝐵
105	3, 51, 104, 54, 58	cbviunf 32491	. . . . . . 7 ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵
106		iunexg 7945	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ V)
107	105, 106	eqeltrid 2833	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 ⦋𝑘 / 𝑗⦌𝐵 ∈ 𝑊) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
108	1, 103, 107	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
109		mptexg 7198	. . . . 5 ⊢ (∪ 𝑗 ∈ 𝐴 𝐵 ∈ V → (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V)
110		f1eq1 6754	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
111		nfcv 2892	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑓
112		nfmpt1 5209	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
113	111, 112	nfeq 2906	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)
114		fveq1 6860	. . . . . . . . 9 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (𝑓‘𝑥) = ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥))
115	114	fveqeq2d 6869	. . . . . . . 8 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((2nd ‘(𝑓‘𝑥)) = 𝑥 ↔ (2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
116	113, 115	ralbid 3251	. . . . . . 7 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → (∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥 ↔ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥))
117	110, 116	anbi12d 632	. . . . . 6 ⊢ (𝑓 = (𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥) ↔ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥)))
118	117	spcegv 3566	. . . . 5 ⊢ ((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩) ∈ V → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)))
119	108, 109, 118	3syl 18	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)))
120	119	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → (((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩):∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘((𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨(𝑔‘𝑥), 𝑥⟩)‘𝑥)) = 𝑥) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)))
121	91, 120	mpd 15	. 2 ⊢ ((𝜑 ∧ (𝑔:∪ 𝑗 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝑥 ∈ ⦋(𝑔‘𝑥) / 𝑗⦌𝐵)) → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥))
122	9, 121	exlimddv 1935	1 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Ⅎwnfc 2877   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  Vcvv 3450  ⦋csb 3865  ∅c0 4299  {csn 4592  ⟨cop 4598  ∪ ciun 4958   ↦ cmpt 5191   × cxp 5639  ⟶wf 6510  –1-1→wf1 6511  ‘cfv 6514  2^nd c2nd 7970

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-reg 9552  ax-inf2 9601  ax-ac2 10423

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-en 8922  df-r1 9724  df-rank 9725  df-card 9899  df-ac 10076

This theorem is referenced by:  aciunf1  32594