Theorem aceq3 5895

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 C_ 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 2639	. . . . 5 |- (x = y -> (f C_ x <-> f C_ y))
2		dmeq 4157	. . . . . 6 |- (x = y -> dom x = dom y)
3	2	fneq2d 4506	. . . . 5 |- (x = y -> (f Fn dom x <-> f Fn dom y))
4	1, 3	anbi12d 690	. . . 4 |- (x = y -> ((f C_ x /\ f Fn dom x) <-> (f C_ y /\ f Fn dom y)))
5	4	exbidv 1657	. . 3 |- (x = y -> (E.f(f C_ x /\ f Fn dom x) <-> E.f(f C_ y /\ f Fn dom y)))
6	5	cbvalv 1696	. 2 |- (A.xE.f(f C_ x /\ f Fn dom x) <-> A.yE.f(f C_ y /\ f Fn dom y))
7		visset 2295	. . . . . . . 8 |- x e. _V
8	7	uniex 3794	. . . . . . . 8 |- U.x e. _V
9	7, 8	xpex 4096	. . . . . . 7 |- (x X. U.x) e. _V
10		simpl 346	. . . . . . . . . 10 |- ((w e. x /\ v e. w) -> w e. x)
11		elunii 3182	. . . . . . . . . . 11 |- ((v e. w /\ w e. x) -> v e. U.x)
12	11	ancoms 484	. . . . . . . . . 10 |- ((w e. x /\ v e. w) -> v e. U.x)
13	10, 12	jca 310	. . . . . . . . 9 |- ((w e. x /\ v e. w) -> (w e. x /\ v e. U.x))
14	13	ssopab2i 3574	. . . . . . . 8 |- {<.w, v>. | (w e. x /\ v e. w)} C_ {<.w, v>. | (w e. x /\ v e. U.x)}
15		df-xp 4000	. . . . . . . 8 |- (x X. U.x) = {<.w, v>. | (w e. x /\ v e. U.x)}
16	14, 15	sseqtr4i 2650	. . . . . . 7 |- {<.w, v>. | (w e. x /\ v e. w)} C_ (x X. U.x)
17	9, 16	ssexi 3456	. . . . . 6 |- {<.w, v>. | (w e. x /\ v e. w)} e. _V
18		sseq2 2639	. . . . . . . 8 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> (f C_ y <-> f C_ {<.w, v>. | (w e. x /\ v e. w)}))
19		dmeq 4157	. . . . . . . . 9 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> dom y = dom {<.w, v>. | (w e. x /\ v e. w)})
20	19	fneq2d 4506	. . . . . . . 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)}))
21	18, 20	anbi12d 690	. . . . . . 7 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> ((f C_ y /\ f Fn dom y) <-> (f C_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)})))
22	21	exbidv 1657	. . . . . 6 |- (y = {<.w, v>. | (w e. x /\ v e. w)} -> (E.f(f C_ y /\ f Fn dom y) <-> E.f(f C_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)})))
23	17, 22	cla4v 2370	. . . . 5 |- (A.yE.f(f C_ y /\ f Fn dom y) -> E.f(f C_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}))
24		fndm 4512	. . . . . . . . . . . . 13 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> dom f = dom {<.w, v>. | (w e. x /\ v e. w)})
25		eleq2 1958	. . . . . . . . . . . . . 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)}))
26		dmopab 4167	. . . . . . . . . . . . . . . 16 |- dom {<.w, v>. | (w e. x /\ v e. w)} = {w | E.v(w e. x /\ v e. w)}
27	26	eleq2i 1961	. . . . . . . . . . . . . . 15 |- (z e. dom {<.w, v>. | (w e. x /\ v e. w)} <-> z e. {w | E.v(w e. x /\ v e. w)})
28		19.42v 1688	. . . . . . . . . . . . . . . 16 |- (E.v(z e. x /\ v e. z) <-> (z e. x /\ E.v v e. z))
29		visset 2295	. . . . . . . . . . . . . . . . 17 |- z e. _V
30		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (w e. x <-> z e. x))
31		eleq2 1958	. . . . . . . . . . . . . . . . . . 19 |- (w = z -> (v e. w <-> v e. z))
32	30, 31	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- (w = z -> ((w e. x /\ v e. w) <-> (z e. x /\ v e. z)))
33	32	exbidv 1657	. . . . . . . . . . . . . . . . 17 |- (w = z -> (E.v(w e. x /\ v e. w) <-> E.v(z e. x /\ v e. z)))
34	29, 33	elab 2403	. . . . . . . . . . . . . . . 16 |- (z e. {w | E.v(w e. x /\ v e. w)} <-> E.v(z e. x /\ v e. z))
35		n0 2884	. . . . . . . . . . . . . . . . 17 |- (z =/= (/) <-> E.v v e. z)
36	35	anbi2i 538	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ z =/= (/)) <-> (z e. x /\ E.v v e. z))
37	28, 34, 36	3bitr4i 200	. . . . . . . . . . . . . . 15 |- (z e. {w | E.v(w e. x /\ v e. w)} <-> (z e. x /\ z =/= (/)))
38	27, 37	bitr2i 191	. . . . . . . . . . . . . 14 |- ((z e. x /\ z =/= (/)) <-> z e. dom {<.w, v>. | (w e. x /\ v e. w)})
39	25, 38	syl6rbbr 598	. . . . . . . . . . . . 13 |- (dom f = dom {<.w, v>. | (w e. x /\ v e. w)} -> ((z e. x /\ z =/= (/)) <-> z e. dom f))
40	24, 39	syl 12	. . . . . . . . . . . 12 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> ((z e. x /\ z =/= (/)) <-> z e. dom f))
41	40	adantl 424	. . . . . . . . . . 11 |- ((f C_ {<.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))
42		funfvima3 4830	. . . . . . . . . . . . 13 |- ((Fun f /\ f C_ {<.w, v>. | (w e. x /\ v e. w)}) -> (z e. dom f -> (f` z) e. ({<.w, v>. | (w e. x /\ v e. w)}"{z})))
43	42	ancoms 484	. . . . . . . . . . . 12 |- ((f C_ {<.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})))
44		fnfun 4510	. . . . . . . . . . . 12 |- (f Fn dom {<.w, v>. | (w e. x /\ v e. w)} -> Fun f)
45	43, 44	sylan2 500	. . . . . . . . . . 11 |- ((f C_ {<.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})))
46	41, 45	sylbid 220	. . . . . . . . . 10 |- ((f C_ {<.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})))
47	46	imp 377	. . . . . . . . 9 |- (((f C_ {<.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}))
48		ibar 705	. . . . . . . . . . . . 13 |- (z e. x -> (u e. z <-> (z e. x /\ u e. z)))
49	48	abbi2dv 2009	. . . . . . . . . . . 12 |- (z e. x -> z = {u | (z e. x /\ u e. z)})
50		imasng 4287	. . . . . . . . . . . . . 14 |- (z e. _V -> ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = {u | z{<.w, v>. | (w e. x /\ v e. w)}u})
51	29, 50	ax-mp 7	. . . . . . . . . . . . 13 |- ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = {u | z{<.w, v>. | (w e. x /\ v e. w)}u}
52		visset 2295	. . . . . . . . . . . . . . 15 |- u e. _V
53		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (v = u -> (v e. z <-> u e. z))
54	53	anbi2d 678	. . . . . . . . . . . . . . 15 |- (v = u -> ((z e. x /\ v e. z) <-> (z e. x /\ u e. z)))
55		eqid 1884	. . . . . . . . . . . . . . 15 |- {<.w, v>. | (w e. x /\ v e. w)} = {<.w, v>. | (w e. x /\ v e. w)}
56	29, 52, 32, 54, 55	brab 3571	. . . . . . . . . . . . . 14 |- (z{<.w, v>. | (w e. x /\ v e. w)}u <-> (z e. x /\ u e. z))
57	56	abbii 2006	. . . . . . . . . . . . 13 |- {u | z{<.w, v>. | (w e. x /\ v e. w)}u} = {u | (z e. x /\ u e. z)}
58	51, 57	eqtri 1908	. . . . . . . . . . . 12 |- ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = {u | (z e. x /\ u e. z)}
59	49, 58	syl6reqr 1947	. . . . . . . . . . 11 |- (z e. x -> ({<.w, v>. | (w e. x /\ v e. w)}"{z}) = z)
60	59	eleq2d 1964	. . . . . . . . . 10 |- (z e. x -> ((f` z) e. ({<.w, v>. | (w e. x /\ v e. w)}"{z}) <-> (f` z) e. z))
61	60	ad2antrl 442	. . . . . . . . 9 |- (((f C_ {<.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}) <-> (f` z) e. z))
62	47, 61	mpbid 212	. . . . . . . 8 |- (((f C_ {<.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. z)
63	62	exp32 408	. . . . . . 7 |- ((f C_ {<.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. z)))
64	63	r19.21aiv 2175	. . . . . 6 |- ((f C_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}) -> A.z e. x (z =/= (/) -> (f` z) e. z))
65	64	eximi 1387	. . . . 5 |- (E.f(f C_ {<.w, v>. | (w e. x /\ v e. w)} /\ f Fn dom {<.w, v>. | (w e. x /\ v e. w)}) -> E.fA.z e. x (z =/= (/) -> (f` z) e. z))
66	23, 65	syl 12	. . . 4 |- (A.yE.f(f C_ y /\ f Fn dom y) -> E.fA.z e. x (z =/= (/) -> (f` z) e. z))
67	66	19.21aiv 1664	. . 3 |- (A.yE.f(f C_ y /\ f Fn dom y) -> A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z))
68		eqid 1884	. . . . 5 |- {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))} = {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))}
69	68	aceq3lem 5894	. . . 4 |- (A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z) -> E.f(f C_ y /\ f Fn dom y))
70	69	19.21aiv 1664	. . 3 |- (A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z) -> A.yE.f(f C_ y /\ f Fn dom y))
71	67, 70	impbii 174	. 2 |- (A.yE.f(f C_ y /\ f Fn dom y) <-> A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z))
72	6, 71	bitri 190	1 |- (A.xE.f(f C_ x /\ f Fn dom x) <-> A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  _Vcvv 2292   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986  "cima 3989  Fun wfun 3992   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  aceq4 5896  aceq5 5902  aceq6a 5903  aceq6b 5904  ac4 5912  ac5 5914

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014

Copyright terms: Public domain