Theorem aceq3 3556

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is similar to the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is the Axiom of Choice of [TakeutiZaring] p. 83. The proof does not depend on AC.

Assertion

Ref	Expression
aceq3	|- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.xE.fA.z e. x (-. z = (/) -> (f` z) e. z))

Distinct variable group(s):   x,f,z

Proof of Theorem aceq3

Step	Hyp	Ref	Expression
1		sseq2 1522	. . . . 5 |- (x = y -> (f (_ x <-> f (_ y))
2		dmeq 2531	. . . . . 6 |- (x = y -> dom x = dom y)
3		fneq2 2719	. . . . . 6 |- (dom x = dom y -> (f Fn dom x <-> f Fn dom y))
4	2, 3	syl 12	. . . . 5 |- (x = y -> (f Fn dom x <-> f Fn dom y))
5	1, 4	anbi12d 476	. . . 4 |- (x = y -> ((f (_ x /\ f Fn dom x) <-> (f (_ y /\ f Fn dom y)))
6	5	biexdv 936	. . 3 |- (x = y -> (E.f(f (_ x /\ f Fn dom x) <-> E.f(f (_ y /\ f Fn dom y)))
7	6	cbvalv 972	. 2 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.yE.f(f (_ y /\ f Fn dom y))
8		visset 1350	. . . . . . . 8 |- x e. V
9	8	uniex 1947	. . . . . . . 8 |- U.x e. V
10	8, 9	xpex 2488	. . . . . . 7 |- (x X. U.x) e. V
11		pm3.26 256	. . . . . . . . . 10 |- ((w e. x /\ v e. w) -> w e. x)
12		elunii 1924	. . . . . . . . . . 11 |- ((v e. w /\ w e. x) -> v e. U.x)
13	12	ancoms 334	. . . . . . . . . 10 |- ((w e. x /\ v e. w) -> v e. U.x)
14	11, 13	jca 236	. . . . . . . . 9 |- ((w e. x /\ v e. w) -> (w e. x /\ v e. U.x))
15	14	ssopab2i 2120	. . . . . . . 8 |- {<.w, v>. | (w e. x /\ v e. w)} (_ {<.w, v>. | (w e. x /\ v e. U.x)}
16		df-xp 2424	. . . . . . . 8 |- (x X. U.x) = {<.w, v>. | (w e. x /\ v e. U.x)}
17	15, 16	sseqtr4 1533	. . . . . . 7 |- {<.w, v>. | (w e. x /\ v e. w)} (_ (x X. U.x)
18	10, 17	ssexi 1701	. . . . . 6 |- {<.w, v>. | (w e. x /\ v e. w)} e. V
19		sseq2 1522	. . . . . . . 8 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> (f (_ y <-> f (_ {<.w, v>. | (w e. x /\ v e. w)}))
20		dmeq 2531	. . . . . . . . 9 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> dom y = dom {<.w, v>. | (w e. x /\ v e. w)})
21		fneq2 2719	. . . . . . . . 9 |- (dom y = dom {<.w, v>. | (w e. x /\ v e. w)} -> (f Fn dom y <-> f Fn dom {<.w, v>. | (w e. x /\ v e. w)}))
22	20, 21	syl 12	. . . . . . . 8 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> (f Fn dom y <-> f Fn dom {<.w, v>. | (w e. x /\ v e. w)}))
23	19, 22	anbi12d 476	. . . . . . 7 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> ((f (_ y /\ f Fn dom y) <-> (f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)})))
24	23	biexdv 936	. . . . . 6 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> (E.f(f (_ y /\ f Fn dom y) <-> E.f(f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)})))
25	18, 24	cla4v 1400	. . . . 5 |- (A.yE.f(f (_ y /\ f Fn dom y) -> E.f(f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}))
26		fndm 2723	. . . . . . . . . . . . 13 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> dom f = dom {<.w, v>. | (w e. x /\ v e. w)})
27		eleq2 1150	. . . . . . . . . . . . . 14 |- (dom f = dom {<.w, v>. | (w e. x /\ v e. w)} -> (z e. dom f <-> z e. dom {<.w, v>. | (w e. x /\ v e. w)}))
28		dmopab 2539	. . . . . . . . . . . . . . . 16 |- dom {<.w, v>. | (w e. x /\ v e. w)} = {w | E.v(w e. x /\ v e. w)}
29	28	eleq2i 1153	. . . . . . . . . . . . . . 15 |- (z e. dom {<.w, v>. | (w e. x /\ v e. w)} <-> z e. {w | E.v(w e. x /\ v e. w)})
30		19.42v 966	. . . . . . . . . . . . . . . 16 |- (E.v(z e. x /\ v e. z) <-> (z e. x /\ E.v v e. z))
31		visset 1350	. . . . . . . . . . . . . . . . 17 |- z e. V
32		eleq1 1149	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (w e. x <-> z e. x))
33		eleq2 1150	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (v e. w <-> v e. z))
34	32, 33	anbi12d 476	. . . . . . . . . . . . . . . . . 18 |- (w = z -> ((w e. x /\ v e. w) <-> (z e. x /\ v e. z)))
35	34	biexdv 936	. . . . . . . . . . . . . . . . 17 |- (w = z -> (E.v(w e. x /\ v e. w) <-> E.v(z e. x /\ v e. z)))
36	31, 35	elab 1415	. . . . . . . . . . . . . . . 16 |- (z e. {w | E.v(w e. x /\ v e. w)} <-> E.v(z e. x /\ v e. z))
37		n0 1714	. . . . . . . . . . . . . . . . 17 |- (-. z = (/) <-> E.v v e. z)
38	37	anbi2i 367	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ -. z = (/)) <-> (z e. x /\ E.v v e. z))
39	30, 36, 38	3bitr4 158	. . . . . . . . . . . . . . 15 |- (z e. {w | E.v(w e. x /\ v e. w)} <-> (z e. x /\ -. z = (/)))
40	29, 39	bitr2 152	. . . . . . . . . . . . . 14 |- ((z e. x /\ -. z = (/)) <-> z e. dom {<.w, v>. | (w e. x /\ v e. w)})
41	27, 40	syl6rbbr 417	. . . . . . . . . . . . 13 |- (dom f = dom {<.w, v>. | (w e. x /\ v e. w)} -> ((z e. x /\ -. z = (/)) <-> z e. dom f))
42	26, 41	syl 12	. . . . . . . . . . . 12 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> ((z e. x /\ -. z = (/)) <-> z e. dom f))
43	42	adantl 305	. . . . . . . . . . 11 |- ((f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}) -> ((z e. x /\ -. z = (/)) <-> z e. dom f))
44		funfvima3 2906	. . . . . . . . . . . . 13 |- ((Fun f /\ f (_ {<.w, v>. | (w e. x /\ v e. w)}) -> (z e. dom f -> (f` z) e. ({<.w, v>. | (w e. x /\ v e. w)}"{z})))
45	44	ancoms 334	. . . . . . . . . . . 12 |- ((f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ Fun f) -> (z e. dom f -> (f` z) e. ({<.w, v>. | (w e. x /\ v e. w)}"{z})))
46		fnfun 2721	. . . . . . . . . . . 12 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> Fun f)
47	45, 46	sylan2 346	. . . . . . . . . . 11 |- ((f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}) -> (z e. dom f -> (f` z) e. ({<.w, v>. | (w e. x /\ v e. w)}"{z})))
48	43, 47	sylbid 178	. . . . . . . . . 10 |- ((f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}) -> ((z e. x /\ -. z = (/)) -> (f` z) e. ({<.w, v>. | (w e. x /\ v e. w)}"{z})))
49	48	imp 277	. . . . . . . . 9 |- (((f (_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}) /\ (z e. x /\ -. z = (/))) -> (f` z) e. ({<.w, v>. | (w e. x /\ v e. w)}"{z}))
50		ibar 487	. . . . . . . . . . . . 13 |- (z e. x -> (u e. z <-> (z e. x /\ u e. z)))
51	50	biabrdv 1184	. . . . . . . . . . . 12 |- (z e. x -> z = {u | (z e. x /\ u e. z)})
52		relopab 2494	. . . . . . . . . . . . . 14 |- Rel {<.w, v>. | (w e. x /\ v e. w)}
53		imasn 2616	. . . . . . . . . . . . . 14 |- (Rel {<.w, v>. | (w e. x /\ v e. w)} -> ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = {u | <.z, u>. e. {<.w, v>. | (w e. x /\ v e. w)}})
54	52, 53	ax-mp 6	. . . . . . . . . . . . 13 |- ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = {u | <.z, u>. e. {<.w, v>. | (w e. x /\ v e. w)}}
55		visset 1350	. . . . . . . . . . . . . . 15 |- u e. V
56		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (v = u -> (v e. z <-> u e. z))
57	56	anbi2d 468	. . . . . . . . . . . . . . 15 |- (v = u -> ((z e. x /\ v e. z) <-> (z e. x /\ u e. z)))
58	31, 55, 34, 57	opelopab 2117	. . . . . . . . . . . . . 14 |- (<.z, u>. e.