Theorem dfac2 8502

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8833). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 8015 and preleq 8025 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 8501.) 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 8493	. . 3 |- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
2		nfra1 2835	. . . . . . 7 |- F/ z A. z e. x ( z =/= (/) -> ( f ` z ) e. z )
3		rsp 2820	. . . . . . . . . . . . 13 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> ( f ` z ) e. z ) ) )
4		equid 1796	. . . . . . . . . . . . . . . . . . 19 |- z = z
5		neeq1 2735	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
6		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u = z <-> z = z ) )
7	5, 6	anbi12d 708	. . . . . . . . . . . . . . . . . . . 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 682	. . . . . . . . . . . . . . . . . 18 |- ( ( z e. x /\ z =/= (/) ) -> E. u e. x ( u =/= (/) /\ u = z ) )
10		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = z -> ( f ` u ) = ( f ` z ) )
11	10	preq1d 4101	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` u ) , u } = { ( f ` z ) , u } )
12		preq2 4096	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` z ) , u } = { ( f ` z ) , z } )
13	11, 12	eqtr2d 2496	. . . . . . . . . . . . . . . . . . . 20 |- ( u = z -> { ( f ` z ) , z } = { ( f ` u ) , u } )
14	13	anim2i 567	. . . . . . . . . . . . . . . . . . 19 |- ( ( u =/= (/) /\ u = z ) -> ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
15	14	reximi 2922	. . . . . . . . . . . . . . . . . 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 4679	. . . . . . . . . . . . . . . . . 18 |- { ( f ` z ) , z } e. _V
18		eqeq1 2458	. . . . . . . . . . . . . . . . . . . 20 |- ( g = { ( f ` z ) , z } -> ( g = { ( f ` u ) , u } <-> { ( f ` z ) , z } = { ( f ` u ) , u } ) )
19	18	anbi2d 701	. . . . . . . . . . . . . . . . . . 19 |- ( g = { ( f ` z ) , z } -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) ) )
20	19	rexbidv 2965	. . . . . . . . . . . . . . . . . 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 4125	. . . . . . . . . . . . . . . . 17 |- z e. { ( f ` z ) , z }
25		fvex 5858	. . . . . . . . . . . . . . . . . 18 |- ( f ` z ) e. _V
26	25	prid1 4124	. . . . . . . . . . . . . . . . 17 |- ( f ` z ) e. { ( f ` z ) , z }
27	24, 26	pm3.2i 453	. . . . . . . . . . . . . . . 16 |- ( z e. { ( f ` z ) , z } /\ ( f ` z ) e. { ( f ` z ) , z } )
28		eleq2 2527	. . . . . . . . . . . . . . . . . 18 |- ( v = { ( f ` z ) , z } -> ( z e. v <-> z e. { ( f ` z ) , z } ) )
29		eleq2 2527	. . . . . . . . . . . . . . . . . 18 |- ( v = { ( f ` z ) , z } -> ( ( f ` z ) e. v <-> ( f ` z ) e. { ( f ` z ) , z } ) )
30	28, 29	anbi12d 708	. . . . . . . . . . . . . . . . 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 660	. . . . . . . . . . . . . . 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 2526	. . . . . . . . . . . . . . . . 17 |- ( w = ( f ` z ) -> ( w e. z <-> ( f ` z ) e. z ) )
34		eleq1 2526	. . . . . . . . . . . . . . . . . . 19 |- ( w = ( f ` z ) -> ( w e. v <-> ( f ` z ) e. v ) )
35	34	anbi2d 701	. . . . . . . . . . . . . . . . . 18 |- ( w = ( f ` z ) -> ( ( z e. v /\ w e. v ) <-> ( z e. v /\ ( f ` z ) e. v ) ) )
36	35	rexbidv 2965	. . . . . . . . . . . . . . . . 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 708	. . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . 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 432	. . . . . . . . . . . . 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 429	. . . . . . . . . . 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 2810	. . . . . . . . . . . . . 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 2458	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = v -> ( g = { ( f ` u ) , u } <-> v = { ( f ` u ) , u } ) )
47	46	anbi2d 701	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = v -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> ( u =/= (/) /\ v = { ( f ` u ) , u } ) ) )
48	47	rexbidv 2965	. . . . . . . . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = u -> ( z =/= (/) <-> u =/= (/) ) )
51		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z = u -> ( f ` z ) = ( f ` u ) )
52	51	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. z ) )
53		eleq2 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 318	. . . . . . . . . . . . . . . . . . . . . . . . . 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 8015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- -. w e. w
58		eleq2 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( w = z -> ( w e. w <-> w e. z ) )
59	57, 58	mtbii 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f ` u ) e. _V
63		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- u e. _V
64	61, 23, 62, 63	prel12 4193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( -. w = z -> ( { w , z } = { ( f ` u ) , u } <-> ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) ) )
65		ancom 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( w e. v /\ z e. v ) <-> ( z e. v /\ w e. v ) )
66		eleq2 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( v = { ( f ` u ) , u } -> ( w e. v <-> w e. { ( f ` u ) , u } ) )
67		eleq2 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( v = { ( f ` u ) , u } -> ( z e. v <-> z e. { ( f ` u ) , u } ) )
68	66, 67	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( v = { ( f ` u ) , u } /\ -. w = z ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
71	60, 70	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( v = { ( f ` u ) , u } /\ w e. z ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
72	71	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z = u -> ( w = ( f ` z ) <-> w = ( f ` u ) ) )
77	76	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 606	. . . . . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . . . . . . . . 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 2940	. . . . . . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . . . . 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 588	. . . . . . . . . . . . . . 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 1729	. . . . . . . . . . . . . 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 601	. . . . . . . . . . . 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 1724	. . . . . . . . . . 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 542	. . . . . . . . 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 2811	. . . . . . . . . 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 2312	. . . . . . . . . 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 434	. . . . . . 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 2854	. . . . . 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 6707	. . . . . . . . . . 11 |- ran f e. _V
106		p0ex 4624	. . . . . . . . . . 11 |- { (/) } e. _V
107	105, 106	unex 6571	. . . . . . . . . 10 |- ( ran f u. { (/) } ) e. _V
108		vex 3109	. . . . . . . . . 10 |- x e. _V
109	107, 108	unex 6571	. . . . . . . . 9 |- ( ( ran f u. { (/) } ) u. x ) e. _V
110	109	pwex 4620	. . . . . . . 8 |- ~P ( ( ran f u. { (/) } ) u. x ) e. _V
111		ssun1 3653	. . . . . . . . . . . . . . 15 |- ( ran f u. { (/) } ) C_ ( ( ran f u. { (/) } ) u. x )
112		fvrn0 5870	. . . . . . . . . . . . . . 15 |- ( f ` u ) e. ( ran f u. { (/) } )
113	111, 112	sselii 3486	. . . . . . . . . . . . . 14 |- ( f ` u ) e. ( ( ran f u. { (/) } ) u. x )
114		elun2 3658	. . . . . . . . . . . . . 14 |- ( u e. x -> u e. ( ( ran f u. { (/) } ) u. x ) )
115		prssi 4172	. . . . . . . . . . . . . 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 661	. . . . . . . . . . . . 13 |- ( u e. x -> { ( f ` u ) , u } C_ ( ( ran f u. { (/) } ) u. x ) )
117		prex 4679	. . . . . . . . . . . . . 14 |- { ( f ` u ) , u } e. _V
118	117	elpw 4005	. . . . . . . . . . . . 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 2526	. . . . . . . . . . . 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 465	. . . . . . . . . 10 |- ( u e. x -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) ) )
123	122	rexlimiv 2940	. . . . . . . . 9 |- ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) )
124	123	abssi 3561	. . . . . . . 8 |- { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } C_ ~P ( ( ran f u. { (/) } ) u. x )
125	110, 124	ssexi 4582	. . . . . . 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 314	. . . . . . . 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 2893	. . . . . . 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 1727	. . . 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 1638	. . 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 8501	. 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 367   A.wal 1396   = wceq 1398   E.wex 1617   e. wcel 1823   E!weu 2284   E*wmo 2285   {cab 2439   =/= wne 2649   A.wral 2804   E.wrex 2805   E!wreu 2806   u. cun 3459   C_ wss 3461   (/)c0 3783   ~Pcpw 3999   {csn 4016   {cpr 4018   ran crn 4989   ` cfv 5570  CHOICEwac 8487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-reg 8010

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-eprel 4780  df-id 4784  df-fr 4827  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-fv 5578  df-riota 6232  df-ac 8488

This theorem is referenced by:  dfac7  8503