Theorem dfac3 8944

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as 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. (Contributed by NM, 24-Mar-2004.) (Revised by Stefan O'Rear, 22-Feb-2015.)

Assertion

Ref	Expression
dfac3	|- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )

Distinct variable group:   x, f, z

Proof of Theorem dfac3

Dummy variables y w v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ac 8939	. 2 |- (CHOICE <-> A. y E. f ( f C_ y /\ f Fn dom y ) )
2		vex 3203	. . . . . . . 8 |- x e. _V
3		vuniex 6954	. . . . . . . 8 |- U. x e. _V
4	2, 3	xpex 6962	. . . . . . 7 |- ( x X. U. x ) e. _V
5		simpl 473	. . . . . . . . . 10 |- ( ( w e. x /\ v e. w ) -> w e. x )
6		elunii 4441	. . . . . . . . . . 11 |- ( ( v e. w /\ w e. x ) -> v e. U. x )
7	6	ancoms 469	. . . . . . . . . 10 |- ( ( w e. x /\ v e. w ) -> v e. U. x )
8	5, 7	jca 554	. . . . . . . . 9 |- ( ( w e. x /\ v e. w ) -> ( w e. x /\ v e. U. x ) )
9	8	ssopab2i 5003	. . . . . . . 8 |- { <. w , v >. | ( w e. x /\ v e. w ) } C_ { <. w , v >. | ( w e. x /\ v e. U. x ) }
10		df-xp 5120	. . . . . . . 8 |- ( x X. U. x ) = { <. w , v >. | ( w e. x /\ v e. U. x ) }
11	9, 10	sseqtr4i 3638	. . . . . . 7 |- { <. w , v >. | ( w e. x /\ v e. w ) } C_ ( x X. U. x )
12	4, 11	ssexi 4803	. . . . . 6 |- { <. w , v >. | ( w e. x /\ v e. w ) } e. _V
13		sseq2 3627	. . . . . . . 8 |- ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( f C_ y <-> f C_ { <. w , v >. | ( w e. x /\ v e. w ) } ) )
14		dmeq 5324	. . . . . . . . 9 |- ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> dom y = dom { <. w , v >. | ( w e. x /\ v e. w ) } )
15	14	fneq2d 5982	. . . . . . . 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 ) } ) )
16	13, 15	anbi12d 747	. . . . . . 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 ) } ) ) )
17	16	exbidv 1850	. . . . . 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 ) } ) ) )
18	12, 17	spcv 3299	. . . . 5 |- ( A. y 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 ) } ) )
19		fndm 5990	. . . . . . . . . . . . 13 |- ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } )
20		eleq2 2690	. . . . . . . . . . . . . 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 ) } ) )
21		dmopab 5335	. . . . . . . . . . . . . . . 16 |- dom { <. w , v >. | ( w e. x /\ v e. w ) } = { w | E. v ( w e. x /\ v e. w ) }
22	21	eleq2i 2693	. . . . . . . . . . . . . . 15 |- ( z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } <-> z e. { w | E. v ( w e. x /\ v e. w ) } )
23		vex 3203	. . . . . . . . . . . . . . . 16 |- z e. _V
24		elequ1 1997	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( w e. x <-> z e. x ) )
25		eleq2 2690	. . . . . . . . . . . . . . . . . 18 |- ( w = z -> ( v e. w <-> v e. z ) )
26	24, 25	anbi12d 747	. . . . . . . . . . . . . . . . 17 |- ( w = z -> ( ( w e. x /\ v e. w ) <-> ( z e. x /\ v e. z ) ) )
27	26	exbidv 1850	. . . . . . . . . . . . . . . 16 |- ( w = z -> ( E. v ( w e. x /\ v e. w ) <-> E. v ( z e. x /\ v e. z ) ) )
28	23, 27	elab 3350	. . . . . . . . . . . . . . 15 |- ( z e. { w | E. v ( w e. x /\ v e. w ) } <-> E. v ( z e. x /\ v e. z ) )
29		19.42v 1918	. . . . . . . . . . . . . . . 16 |- ( E. v ( z e. x /\ v e. z ) <-> ( z e. x /\ E. v v e. z ) )
30		n0 3931	. . . . . . . . . . . . . . . . 17 |- ( z =/= (/) <-> E. v v e. z )
31	30	anbi2i 730	. . . . . . . . . . . . . . . 16 |- ( ( z e. x /\ z =/= (/) ) <-> ( z e. x /\ E. v v e. z ) )
32	29, 31	bitr4i 267	. . . . . . . . . . . . . . 15 |- ( E. v ( z e. x /\ v e. z ) <-> ( z e. x /\ z =/= (/) ) )
33	22, 28, 32	3bitrri 287	. . . . . . . . . . . . . 14 |- ( ( z e. x /\ z =/= (/) ) <-> z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } )
34	20, 33	syl6rbbr 279	. . . . . . . . . . . . 13 |- ( dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) )
35	19, 34	syl 17	. . . . . . . . . . . 12 |- ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) )
36	35	adantl 482	. . . . . . . . . . 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 ) )
37		fnfun 5988	. . . . . . . . . . . 12 |- ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> Fun f )
38		funfvima3 6495	. . . . . . . . . . . . 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 } ) ) )
39	38	ancoms 469	. . . . . . . . . . . 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 } ) ) )
40	37, 39	sylan2 491	. . . . . . . . . . 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 } ) ) )
41	36, 40	sylbid 230	. . . . . . . . . 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 } ) ) )
42	41	imp 445	. . . . . . . . 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 } ) )
43		ibar 525	. . . . . . . . . . . . 13 |- ( z e. x -> ( u e. z <-> ( z e. x /\ u e. z ) ) )
44	43	abbi2dv 2742	. . . . . . . . . . . 12 |- ( z e. x -> z = { u | ( z e. x /\ u e. z ) } )
45		imasng 5487	. . . . . . . . . . . . . 14 |- ( z e. _V -> ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u } )
46	23, 45	ax-mp 5	. . . . . . . . . . . . 13 |- ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u }
47		vex 3203	. . . . . . . . . . . . . . 15 |- u e. _V
48		elequ1 1997	. . . . . . . . . . . . . . . 16 |- ( v = u -> ( v e. z <-> u e. z ) )
49	48	anbi2d 740	. . . . . . . . . . . . . . 15 |- ( v = u -> ( ( z e. x /\ v e. z ) <-> ( z e. x /\ u e. z ) ) )
50		eqid 2622	. . . . . . . . . . . . . . 15 |- { <. w , v >. | ( w e. x /\ v e. w ) } = { <. w , v >. | ( w e. x /\ v e. w ) }
51	23, 47, 26, 49, 50	brab 4998	. . . . . . . . . . . . . 14 |- ( z { <. w , v >. | ( w e. x /\ v e. w ) } u <-> ( z e. x /\ u e. z ) )
52	51	abbii 2739	. . . . . . . . . . . . 13 |- { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u } = { u | ( z e. x /\ u e. z ) }
53	46, 52	eqtri 2644	. . . . . . . . . . . 12 |- ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | ( z e. x /\ u e. z ) }
54	44, 53	syl6reqr 2675	. . . . . . . . . . 11 |- ( z e. x -> ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = z )
55	54	eleq2d 2687	. . . . . . . . . 10 |- ( z e. x -> ( ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) <-> ( f ` z ) e. z ) )
56	55	ad2antrl 764	. . . . . . . . 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 ) )
57	42, 56	mpbid 222	. . . . . . . 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 )
58	57	exp32 631	. . . . . . 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 ) ) )
59	58	ralrimiv 2965	. . . . . 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 ) )
60	59	eximi 1762	. . . . 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. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
61	18, 60	syl 17	. . . 4 |- ( A. y E. f ( f C_ y /\ f Fn dom y ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
62	61	alrimiv 1855	. . 3 |- ( A. y E. f ( f C_ y /\ f Fn dom y ) -> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
63		eqid 2622	. . . . 5 |- ( w e. dom y |-> ( f ` { u | w y u } ) ) = ( w e. dom y |-> ( f ` { u | w y u } ) )
64	63	aceq3lem 8943	. . . 4 |- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. f ( f C_ y /\ f Fn dom y ) )
65	64	alrimiv 1855	. . 3 |- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. y E. f ( f C_ y /\ f Fn dom y ) )
66	62, 65	impbii 199	. 2 |- ( A. y E. f ( f C_ y /\ f Fn dom y ) <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
67	1, 66	bitri 264	1 |- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   _Vcvv 3200   C_ wss 3574   (/)c0 3915   {csn 4177   U.cuni 4436   class class class wbr 4653   {copab 4712   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   "cima 5117   Fun wfun 5882   Fn wfn 5883   ` cfv 5888  CHOICEwac 8938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-ac 8939

This theorem is referenced by:  dfac4  8945  dfac5  8951  dfac2a  8952  dfac2  8953  dfac8  8957  dfac9  8958  ac4  9297  dfac11  37632