Theorem aceq3 4705

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:   x,f,z

Proof of Theorem aceq3

Step	Hyp	Ref	Expression
1		sseq2 2073	. . . . 5 |- (x = y -> (f (_ x <-> f (_ y))
2		dmeq 3300	. . . . . 6 |- (x = y -> dom x = dom y)
3		fneq2 3569	. . . . . 6 |- (dom x = dom y -> (f Fn dom x <-> f Fn dom y))
4	2, 3	syl 10	. . . . 5 |- (x = y -> (f Fn dom x <-> f Fn dom y))
5	1, 4	anbi12d 626	. . . 4 |- (x = y -> ((f (_ x /\ f Fn dom x) <-> (f (_ y /\ f Fn dom y)))
6	5	exbidv 1274	. . 3 |- (x = y -> (E.f(f (_ x /\ f Fn dom x) <-> E.f(f (_ y /\ f Fn dom y)))
7	6	cbvalv 1309	. 2 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.yE.f(f (_ y /\ f Fn dom y))
8		visset 1804	. . . . . . . 8 |- x e. V
9	8	uniex 2861	. . . . . . . 8 |- U.x e. V
10	8, 9	xpex 3250	. . . . . . 7 |- (x X. U.x) e. V
11		pm3.26 319	. . . . . . . . . 10 |- ((w e. x /\ v e. w) -> w e. x)
12		elunii 2498	. . . . . . . . . . 11 |- ((v e. w /\ w e. x) -> v e. U.x)
13	12	ancoms 436	. . . . . . . . . 10 |- ((w e. x /\ v e. w) -> v e. U.x)
14	11, 13	jca 288	. . . . . . . . 9 |- ((w e. x /\ v e. w) -> (w e. x /\ v e. U.x))
15	14	ssopab2i 2812	. . . . . . . 8 |- {<.w, v>. | (w e. x /\ v e. w)} (_ {<.w, v>. | (w e. x /\ v e. U.x)}
16		df-xp 3174	. . . . . . . 8 |- (x X. U.x) = {<.w, v>. | (w e. x /\ v e. U.x)}
17	15, 16	sseqtr4 2084	. . . . . . 7 |- {<.w, v>. | (w e. x /\ v e. w)} (_ (x X. U.x)
18	10, 17	ssexi 2710	. . . . . 6 |- {<.w, v>. | (w e. x /\ v e. w)} e. V
19		sseq2 2073	. . . . . . . 8 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> (f (_ y <-> f (_ {<.w, v>. | (w e. x /\ v e. w)}))
20		dmeq 3300	. . . . . . . . 9 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> dom y = dom {<.w, v>. | (w e. x /\ v e. w)})
21		fneq2 3569	. . . . . . . . 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 10	. . . . . . . 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 626	. . . . . . 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	exbidv 1274	. . . . . 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 1859	. . . . 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 3573	. . . . . . . . . . . . 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 1527	. . . . . . . . . . . . . 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 3309	. . . . . . . . . . . . . . . 16 |- dom {<.w, v>. | (w e. x /\ v e. w)} = {w | E.v(w e. x /\ v e. w)}
29	28	eleq2i 1530	. . . . . . . . . . . . . . 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 1303	. . . . . . . . . . . . . . . 16 |- (E.v(z e. x /\ v e. z) <-> (z e. x /\ E.v v e. z))
31		visset 1804	. . . . . . . . . . . . . . . . 17 |- z e. V
32		eleq1 1526	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (w e. x <-> z e. x))
33		eleq2 1527	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (v e. w <-> v e. z))
34	32, 33	anbi12d 626	. . . . . . . . . . . . . . . . . 18 |- (w = z -> ((w e. x /\ v e. w) <-> (z e. x /\ v e. z)))
35	34	exbidv 1274	. . . . . . . . . . . . . . . . 17 |- (w = z -> (E.v(w e. x /\ v e. w) <-> E.v(z e. x /\ v e. z)))
36	31, 35	elab 1888	. . . . . . . . . . . . . . . 16 |- (z e. {w | E.v(w e. x /\ v e. w)} <-> E.v(z e. x /\ v e. z))
37		ne0 2278	. . . . . . . . . . . . . . . . 17 |- (z =/= (/) <-> E.v v e. z)
38	37	anbi2i 479	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ z =/= (/)) <-> (z e. x /\ E.v v e. z))
39	30, 36, 38	3bitr4 183	. . . . . . . . . . . . . . 15 |- (z e. {w | E.v(w e. x /\ v e. w)} <-> (z e. x /\ z =/= (/)))
40	29, 39	bitr2 174	. . . . . . . . . . . . . 14 |- ((z e. x /\ z =/= (/)) <-> z e. dom {<.w, v>. | (w e. x /\ v e. w)})
41	27, 40	syl6rbbr 537	. . . . . . . . . . . . 13 |- (dom f = dom {<.w, v>. | (w e. x /\ v e. w)} -> ((z e. x /\ z =/= (/)) <-> z e. dom f))
42	26, 41	syl 10	. . . . . . . . . . . 12 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> ((z e. x /\ z =/= (/)) <-> z e. dom f))
43	42	adantl 388	. . . . . . . . . . 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 3839	. . . . . . . . . . . . 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 436	. . . . . . . . . . . 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 3571	. . . . . . . . . . . 12 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> Fun f)
47	45, 46	sylan2 451	. . . . . . . . . . 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 203	. . . . . . . . . 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 350	. . . . . . . . 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 641	. . . . . . . . . . . . 13 |- (z e. x -> (u e. z <-> (z e. x /\ u e. z)))
51	50	abbi2dv 1570	. . . . . . . . . . . 12 |- (z e. x -> z = {u | (z e. x /\ u e. z)})
52		imasng 3408	. . . . . . . . . . . . . 14 |- (z e. V -> ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = {u | z{<.w, v>. | (w e. x /\ v e. w)}u})
53	31, 52	ax-mp 7	. . . . . . . . . . . . 13 |- ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = {u | z{<.w, v>. | (w e. x /\ v e. w)}u}
54		visset 1804	. . . . . . . . . . . . . . 15 |- u e. V
55		eleq1 1526	. . . . . . . . . . . . . . . 16 |- (v = u -> (v e. z <-> u e. z))
56	55	anbi2d 614	. . . . . . . . . . . . . . 15 |- (v = u -> ((z e. x /\ v e. z) <-> (z e. x /\ u e. z)))
57