Theorem aceq3 4733

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 2083	. . . . 5 |- (x = y -> (f (_ x <-> f (_ y))
2		dmeq 3311	. . . . . 6 |- (x = y -> dom x = dom y)
3		fneq2 3583	. . . . . 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 628	. . . 4 |- (x = y -> ((f (_ x /\ f Fn dom x) <-> (f (_ y /\ f Fn dom y)))
6	5	exbidv 1279	. . 3 |- (x = y -> (E.f(f (_ x /\ f Fn dom x) <-> E.f(f (_ y /\ f Fn dom y)))
7	6	cbvalv 1314	. 2 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.yE.f(f (_ y /\ f Fn dom y))
8		visset 1813	. . . . . . . 8 |- x e. V
9	8	uniex 2870	. . . . . . . 8 |- U.x e. V
10	8, 9	xpex 3260	. . . . . . 7 |- (x X. U.x) e. V
11		pm3.26 319	. . . . . . . . . 10 |- ((w e. x /\ v e. w) -> w e. x)
12		elunii 2508	. . . . . . . . . . 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 2823	. . . . . . . 8 |- {<.w, v>. | (w e. x /\ v e. w)} (_ {<.w, v>. | (w e. x /\ v e. U.x)}
16		df-xp 3184	. . . . . . . 8 |- (x X. U.x) = {<.w, v>. | (w e. x /\ v e. U.x)}
17	15, 16	sseqtr4 2094	. . . . . . 7 |- {<.w, v>. | (w e. x /\ v e. w)} (_ (x X. U.x)
18	10, 17	ssexi 2720	. . . . . 6 |- {<.w, v>. | (w e. x /\ v e. w)} e. V
19		sseq2 2083	. . . . . . . 8 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> (f (_ y <-> f (_ {<.w, v>. | (w e. x /\ v e. w)}))
20		dmeq 3311	. . . . . . . . 9 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> dom y = dom {<.w, v>. | (w e. x /\ v e. w)})
21		fneq2 3583	. . . . . . . . 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 628	. . . . . . 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 1279	. . . . . 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 1868	. . . . 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 3587	. . . . . . . . . . . . 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 1535	. . . . . . . . . . . . . 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 3320	. . . . . . . . . . . . . . . 16 |- dom {<.w, v>. | (w e. x /\ v e. w)} = {w | E.v(w e. x /\ v e. w)}
29	28	eleq2i 1538	. . . . . . . . . . . . . . 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 1308	. . . . . . . . . . . . . . . 16 |- (E.v(z e. x /\ v e. z) <-> (z e. x /\ E.v v e. z))
31		visset 1813	. . . . . . . . . . . . . . . . 17 |- z e. V
32		eleq1 1534	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (w e. x <-> z e. x))
33		eleq2 1535	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (v e. w <-> v e. z))
34	32, 33	anbi12d 628	. . . . . . . . . . . . . . . . . 18 |- (w = z -> ((w e. x /\ v e. w) <-> (z e. x /\ v e. z)))
35	34	exbidv 1279	. . . . . . . . . . . . . . . . 17 |- (w = z -> (E.v(w e. x /\ v e. w) <-> E.v(z e. x /\ v e. z)))
36	31, 35	elab 1897	. . . . . . . . . . . . . . . 16 |- (z e. {w | E.v(w e. x /\ v e. w)} <-> E.v(z e. x /\ v e. z))
37		ne0 2288	. . . . . . . . . . . . . . . . 17 |- (z =/= (/) <-> E.v v e. z)
38	37	anbi2i 480	. . . . . . . . . . . . . . . 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 539	. . . . . . . . . . . . 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 3854	. . . . . . . . . . . . 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 3585	. . . . . . . . . . . 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 643	. . . . . . . . . . . . 13 |- (z e. x -> (u e. z <-> (z e. x /\ u e. z)))
51	50	abbi2dv 1578	. . . . . . . . . . . 12 |- (z e. x -> z = {u | (z e. x /\ u e. z)})
52		imasng 3424	. . . . . . . . . . . . . 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 1813	. . . . . . . . . . . . . . 15 |- u e. V
55		eleq1 1534	. . . . . . . . . . . . . . . 16 |- (v = u -> (v e. z <-> u e. z))
56	55	anbi2d 616	. . . . . . . . . . . . . . 15 |- (v = u -> ((z e. x /\ v e. z) <-> (z e. x /\ u e. z)))