Theorem dfac2 8500

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8831). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 8012 and preleq 8023 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a 8499.) TODO: Fix label in comment, and put label changes into list at top of set.mm. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)

Assertion

Ref	Expression
dfac2	|- (CHOICE <-> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )

Distinct variable group:   x, y, z, w, v

Proof of Theorem dfac2

Dummy variables u f g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfac3 8491	. . 3 |- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
2		nfra1 2838	. . . . . . 7 |- F/ z A. z e. x ( z =/= (/) -> ( f ` z ) e. z )
3		rsp 2823	. . . . . . . . . . . . 13 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> ( f ` z ) e. z ) ) )
4		equid 1735	. . . . . . . . . . . . . . . . . . 19 |- z = z
5		neeq1 2741	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
6		eqeq1 2464	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u = z <-> z = z ) )
7	5, 6	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 |- ( u = z -> ( ( u =/= (/) /\ u = z ) <-> ( z =/= (/) /\ z = z ) ) )
8	7	rspcev 3207	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. x /\ ( z =/= (/) /\ z = z ) ) -> E. u e. x ( u =/= (/) /\ u = z ) )
9	4, 8	mpanr2 684	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. x /\ z =/= (/) ) -> E. u e. x ( u =/= (/) /\ u = z ) )
10		fveq2 5857	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = z -> ( f ` u ) = ( f ` z ) )
11	10	preq1d 4105	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` u ) , u } = { ( f ` z ) , u } )
12		preq2 4100	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` z ) , u } = { ( f ` z ) , z } )
13	11, 12	eqtr2d 2502	. . . . . . . . . . . . . . . . . . . 20 |- ( u = z -> { ( f ` z ) , z } = { ( f ` u ) , u } )
14	13	anim2i 569	. . . . . . . . . . . . . . . . . . 19 |- ( ( u =/= (/) /\ u = z ) -> ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
15	14	reximi 2925	. . . . . . . . . . . . . . . . . 18 |- ( E. u e. x ( u =/= (/) /\ u = z ) -> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
16	9, 15	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( z e. x /\ z =/= (/) ) -> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
17		prex 4682	. . . . . . . . . . . . . . . . . 18 |- { ( f ` z ) , z } e. _V
18		eqeq1 2464	. . . . . . . . . . . . . . . . . . . 20 |- ( g = { ( f ` z ) , z } -> ( g = { ( f ` u ) , u } <-> { ( f ` z ) , z } = { ( f ` u ) , u } ) )
19	18	anbi2d 703	. . . . . . . . . . . . . . . . . . 19 |- ( g = { ( f ` z ) , z } -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) ) )
20	19	rexbidv 2966	. . . . . . . . . . . . . . . . . 18 |- ( g = { ( f ` z ) , z } -> ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) ) )
21	17, 20	elab 3243	. . . . . . . . . . . . . . . . 17 |- ( { ( f ` z ) , z } e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } <-> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
22	16, 21	sylibr 212	. . . . . . . . . . . . . . . 16 |- ( ( z e. x /\ z =/= (/) ) -> { ( f ` z ) , z } e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } )
23		vex 3109	. . . . . . . . . . . . . . . . . 18 |- z e. _V
24	23	prid2 4129	. . . . . . . . . . . . . . . . 17 |- z e. { ( f ` z ) , z }
25		fvex 5867	. . . . . . . . . . . . . . . . . 18 |- ( f ` z ) e. _V
26	25	prid1 4128	. . . . . . . . . . . . . . . . 17 |- ( f ` z ) e. { ( f ` z ) , z }
27	24, 26	pm3.2i 455	. . . . . . . . . . . . . . . 16 |- ( z e. { ( f ` z ) , z } /\ ( f ` z ) e. { ( f ` z ) , z } )
28		eleq2 2533	. . . . . . . . . . . . . . . . . 18 |- ( v = { ( f ` z ) , z } -> ( z e. v <-> z e. { ( f ` z ) , z } ) )
29		eleq2 2533	. . . . . . . . . . . . . . . . . 18 |- ( v = { ( f ` z ) , z } -> ( ( f ` z ) e. v <-> ( f ` z ) e. { ( f ` z ) , z } ) )
30	28, 29	anbi12d 710	. . . . . . . . . . . . . . . . 17 |- ( v = { ( f ` z ) , z } -> ( ( z e. v /\ ( f ` z ) e. v ) <-> ( z e. { ( f ` z ) , z } /\ ( f ` z ) e. { ( f ` z ) , z } ) ) )
31	30	rspcev 3207	. . . . . . . . . . . . . . . 16 |- ( ( { ( f ` z ) , z } e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. { ( f ` z ) , z } /\ ( f ` z ) e. { ( f ` z ) , z } ) ) -> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) )
32	22, 27, 31	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ( z e. x /\ z =/= (/) ) -> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) )
33		eleq1 2532	. . . . . . . . . . . . . . . . 17 |- ( w = ( f ` z ) -> ( w e. z <-> ( f ` z ) e. z ) )
34		eleq1 2532	. . . . . . . . . . . . . . . . . . 19 |- ( w = ( f ` z ) -> ( w e. v <-> ( f ` z ) e. v ) )
35	34	anbi2d 703	. . . . . . . . . . . . . . . . . 18 |- ( w = ( f ` z ) -> ( ( z e. v /\ w e. v ) <-> ( z e. v /\ ( f ` z ) e. v ) ) )
36	35	rexbidv 2966	. . . . . . . . . . . . . . . . 17 |- ( w = ( f ` z ) -> ( E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) ) )
37	33, 36	anbi12d 710	. . . . . . . . . . . . . . . 16 |- ( w = ( f ` z ) -> ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) <-> ( ( f ` z ) e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) ) ) )
38	25, 37	spcev 3198	. . . . . . . . . . . . . . 15 |- ( ( ( f ` z ) e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
39	32, 38	sylan2 474	. . . . . . . . . . . . . 14 |- ( ( ( f ` z ) e. z /\ ( z e. x /\ z =/= (/) ) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
40	39	ex 434	. . . . . . . . . . . . 13 |- ( ( f ` z ) e. z -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
41	3, 40	syl8 70	. . . . . . . . . . . 12 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) ) ) )
42	41	impd 431	. . . . . . . . . . 11 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) ) )
43	42	pm2.43d 48	. . . . . . . . . 10 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
44		df-rex 2813	. . . . . . . . . . . . . 14 |- ( E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> E. v ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. v /\ w e. v ) ) )
45		vex 3109	. . . . . . . . . . . . . . . . . . . 20 |- v e. _V
46		eqeq1 2464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = v -> ( g = { ( f ` u ) , u } <-> v = { ( f ` u ) , u } ) )
47	46	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = v -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> ( u =/= (/) /\ v = { ( f ` u ) , u } ) ) )
48	47	rexbidv 2966	. . . . . . . . . . . . . . . . . . . 20 |- ( g = v -> ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) ) )
49	45, 48	elab 3243	. . . . . . . . . . . . . . . . . . 19 |- ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } <-> E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) )
50		neeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = u -> ( z =/= (/) <-> u =/= (/) ) )
51		fveq2 5857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z = u -> ( f ` z ) = ( f ` u ) )
52	51	eleq1d 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. z ) )
53		eleq2 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = u -> ( ( f ` u ) e. z <-> ( f ` u ) e. u ) )
54	52, 53	bitrd 253	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. u ) )
55	50, 54	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = u -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( u =/= (/) -> ( f ` u ) e. u ) ) )
56	55	rspccv 3204	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( f ` u ) e. u ) ) )
57		elirrv 8012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- -. w e. w
58		eleq2 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( w = z -> ( w e. w <-> w e. z ) )
59	57, 58	mtbii 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( w = z -> -. w e. z )
60	59	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( w e. z -> -. w = z )
61		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- w e. _V
62		fvex 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f ` u ) e. _V
63		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- u e. _V
64	61, 23, 62, 63	prel12 4196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. w = z -> ( { w , z } = { ( f ` u ) , u } <-> ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) ) )
65		ancom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( w e. v /\ z e. v ) <-> ( z e. v /\ w e. v ) )
66		eleq2 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( v = { ( f ` u ) , u } -> ( w e. v <-> w e. { ( f ` u ) , u } ) )
67		eleq2 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( v = { ( f ` u ) , u } -> ( z e. v <-> z e. { ( f ` u ) , u } ) )
68	66, 67	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( v = { ( f ` u ) , u } -> ( ( w e. v /\ z e. v ) <-> ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) ) )
69	65, 68	syl5rbbr 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( v = { ( f ` u ) , u } -> ( ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) <-> ( z e. v /\ w e. v ) ) )
70	64, 69	sylan9bbr 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( v = { ( f ` u ) , u } /\ -. w = z ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
71	60, 70	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( v = { ( f ` u ) , u } /\ w e. z ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
72	71	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( v = { ( f ` u ) , u } /\ ( w e. z /\ ( f ` u ) e. u ) ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
73	72	pm5.32da 641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( v = { ( f ` u ) , u } -> ( ( ( w e. z /\ ( f ` u ) e. u ) /\ { w , z } = { ( f ` u ) , u } ) <-> ( ( w e. z /\ ( f ` u ) e. u ) /\ ( z e. v /\ w e. v ) ) ) )
74	61, 23, 62, 63	preleq 8023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( w e. z /\ ( f ` u ) e. u ) /\ { w , z } = { ( f ` u ) , u } ) -> ( w = ( f ` u ) /\ z = u ) )
75	73, 74	syl6bir 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( v = { ( f ` u ) , u } -> ( ( ( w e. z /\ ( f ` u ) e. u ) /\ ( z e. v /\ w e. v ) ) -> ( w = ( f ` u ) /\ z = u ) ) )
76	51	eqeq2d 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z = u -> ( w = ( f ` z ) <-> w = ( f ` u ) ) )
77	76	biimparc 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( w = ( f ` u ) /\ z = u ) -> w = ( f ` z ) )
78	75, 77	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( v = { ( f ` u ) , u } -> ( ( ( w e. z /\ ( f ` u ) e. u ) /\ ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
79	78	exp4c 608	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = { ( f ` u ) , u } -> ( w e. z -> ( ( f ` u ) e. u -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
80	79	com13 80	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f ` u ) e. u -> ( w e. z -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
81	56, 80	syl8 70	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( w e. z -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) ) ) )
82	81	com4r 86	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w e. z -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) ) ) )
83	82	imp 429	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( u e. x -> ( u =/= (/) -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) ) )
84	83	imp4a 589	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( u e. x -> ( ( u =/= (/) /\ v = { ( f ` u ) , u } ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
85	84	com3l 81	. . . . . . . . . . . . . . . . . . . 20 |- ( u e. x -> ( ( u =/= (/) /\ v = { ( f ` u ) , u } ) -> ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
86	85	rexlimiv 2942	. . . . . . . . . . . . . . . . . . 19 |- ( E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) -> ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) )
87	49, 86	sylbi 195	. . . . . . . . . . . . . . . . . 18 |- ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) )
88	87	expd 436	. . . . . . . . . . . . . . . . 17 |- ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( w e. z -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
89	88	com13 80	. . . . . . . . . . . . . . . 16 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( w e. z -> ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
90	89	imp4b 590	. . . . . . . . . . . . . . 15 |- ( ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. z ) -> ( ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
91	90	exlimdv 1695	. . . . . . . . . . . . . 14 |- ( ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. z ) -> ( E. v ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
92	44, 91	syl5bi 217	. . . . . . . . . . . . 13 |- ( ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. z ) -> ( E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) -> w = ( f ` z ) ) )
93	92	expimpd 603	. . . . . . . . . . . 12 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
94	93	alrimiv 1690	. . . . . . . . . . 11 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. w ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
95		mo2icl 3275	. . . . . . . . . . 11 |- ( A. w ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) -> E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
96	94, 95	syl 16	. . . . . . . . . 10 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
97	43, 96	jctird 544	. . . . . . . . 9 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> ( E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) /\ E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) ) )
98		df-reu 2814	. . . . . . . . . 10 |- ( E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> E! w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
99		eu5 2298	. . . . . . . . . 10 |- ( E! w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) <-> ( E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) /\ E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
100	98, 99	bitri 249	. . . . . . . . 9 |- ( E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> ( E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) /\ E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
101	97, 100	syl6ibr 227	. . . . . . . 8 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
102	101	expd 436	. . . . . . 7 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
103	2, 102	ralrimi 2857	. . . . . 6 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. z e. x ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
104		vex 3109	. . . . . . . . . . . 12 |- f e. _V
105	104	rnex 6708	. . . . . . . . . . 11 |- ran f e. _V
106		p0ex 4627	. . . . . . . . . . 11 |- { (/) } e. _V
107	105, 106	unex 6573	. . . . . . . . . 10 |- ( ran f u. { (/) } ) e. _V
108		vex 3109	. . . . . . . . . 10 |- x e. _V
109	107, 108	unex 6573	. . . . . . . . 9 |- ( ( ran f u. { (/) } ) u. x ) e. _V
110	109	pwex 4623	. . . . . . . 8 |- ~P ( ( ran f u. { (/) } ) u. x ) e. _V
111		ssun1 3660	. . . . . . . . . . . . . . 15 |- ( ran f u. { (/) } ) C_ ( ( ran f u. { (/) } ) u. x )
112		fvrn0 5879	. . . . . . . . . . . . . . 15 |- ( f ` u ) e. ( ran f u. { (/) } )
113	111, 112	sselii 3494	. . . . . . . . . . . . . 14 |- ( f ` u ) e. ( ( ran f u. { (/) } ) u. x )
114		elun2 3665	. . . . . . . . . . . . . 14 |- ( u e. x -> u e. ( ( ran f u. { (/) } ) u. x ) )
115		prssi 4176	. . . . . . . . . . . . . 14 |- ( ( ( f ` u ) e. ( ( ran f u. { (/) } ) u. x ) /\ u e. ( ( ran f u. { (/) } ) u. x ) ) -> { ( f ` u ) , u } C_ ( ( ran f u. { (/) } ) u. x ) )
116	113, 114, 115	sylancr 663	. . . . . . . . . . . . 13 |- ( u e. x -> { ( f ` u ) , u } C_ ( ( ran f u. { (/) } ) u. x ) )
117		prex 4682	. . . . . . . . . . . . . 14 |- { ( f ` u ) , u } e. _V
118	117	elpw 4009	. . . . . . . . . . . . 13 |- ( { ( f ` u ) , u } e. ~P ( ( ran f u. { (/) } ) u. x ) <-> { ( f ` u ) , u } C_ ( ( ran f u. { (/) } ) u. x ) )
119	116, 118	sylibr 212	. . . . . . . . . . . 12 |- ( u e. x -> { ( f ` u ) , u } e. ~P ( ( ran f u. { (/) } ) u. x ) )
120		eleq1 2532	. . . . . . . . . . . 12 |- ( g = { ( f ` u ) , u } -> ( g e. ~P ( ( ran f u. { (/) } ) u. x ) <-> { ( f ` u ) , u } e. ~P ( ( ran f u. { (/) } ) u. x ) ) )
121	119, 120	syl5ibrcom 222	. . . . . . . . . . 11 |- ( u e. x -> ( g = { ( f ` u ) , u } -> g e. ~P ( ( ran f u. { (/) } ) u. x ) ) )
122	121	adantld 467	. . . . . . . . . 10 |- ( u e. x -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) ) )
123	122	rexlimiv 2942	. . . . . . . . 9 |- ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) )
124	123	abssi 3568	. . . . . . . 8 |- { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } C_ ~P ( ( ran f u. { (/) } ) u. x )
125	110, 124	ssexi 4585	. . . . . . 7 |- { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } e. _V
126		rexeq 3052	. . . . . . . . . 10 |- ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( E. v e. y ( z e. v /\ w e. v ) <-> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
127	126	reubidv 3039	. . . . . . . . 9 |- ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( E! w e. z E. v e. y ( z e. v /\ w e. v ) <-> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
128	127	imbi2d 316	. . . . . . . 8 |- ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) <-> ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
129	128	ralbidv 2896	. . . . . . 7 |- ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) <-> A. z e. x ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
130	125, 129	spcev 3198	. . . . . 6 |- ( A. z e. x ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
131	103, 130	syl 16	. . . . 5 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
132	131	exlimiv 1693	. . . 4 |- ( E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
133	132	alimi 1609	. . 3 |- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
134	1, 133	sylbi 195	. 2 |- (CHOICE -> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
135		dfac2a 8499	. 2 |- ( A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> CHOICE )
136	134, 135	impbii 188	1 |- (CHOICE <-> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1372   = wceq 1374   E.wex 1591   e. wcel 1762   E!weu 2268   E*wmo 2269   {cab 2445   =/= wne 2655   A.wral 2807   E.wrex 2808   E!wreu 2809   u. cun 3467   C_ wss 3469   (/)c0 3778   ~Pcpw 4003   {csn 4020   {cpr 4022   ran crn 4993   ` cfv 5579  CHOICEwac 8485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-reg 8007

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-eprel 4784  df-id 4788  df-fr 4831  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587  df-riota 6236  df-ac 8486

This theorem is referenced by:  dfac7  8501