Theorem dfac2 8303

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8634). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 7815 and preleq 7826 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 8302.) 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 8294	. . 3 |- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
2		nfra1 2769	. . . . . . 7 |- F/ z A. z e. x ( z =/= (/) -> ( f ` z ) e. z )
3		rsp 2779	. . . . . . . . . . . . 13 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> ( f ` z ) e. z ) ) )
4		equid 1729	. . . . . . . . . . . . . . . . . . 19 |- z = z
5		neeq1 2619	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
6		eqeq1 2449	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u = z <-> z = z ) )
7	5, 6	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 |- ( u = z -> ( ( u =/= (/) /\ u = z ) <-> ( z =/= (/) /\ z = z ) ) )
8	7	rspcev 3076	. . . . . . . . . . . . . . . . . . 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 5694	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = z -> ( f ` u ) = ( f ` z ) )
11	10	preq1d 3963	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` u ) , u } = { ( f ` z ) , u } )
12		preq2 3958	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` z ) , u } = { ( f ` z ) , z } )
13	11, 12	eqtr2d 2476	. . . . . . . . . . . . . . . . . . . 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 2826	. . . . . . . . . . . . . . . . . 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 4537	. . . . . . . . . . . . . . . . . 18 |- { ( f ` z ) , z } e. _V
18		eqeq1 2449	. . . . . . . . . . . . . . . . . . . 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 2739	. . . . . . . . . . . . . . . . . 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 3109	. . . . . . . . . . . . . . . . 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 2978	. . . . . . . . . . . . . . . . . 18 |- z e. _V
24	23	prid2 3987	. . . . . . . . . . . . . . . . 17 |- z e. { ( f ` z ) , z }
25		fvex 5704	. . . . . . . . . . . . . . . . . 18 |- ( f ` z ) e. _V
26	25	prid1 3986	. . . . . . . . . . . . . . . . 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 2504	. . . . . . . . . . . . . . . . . 18 |- ( v = { ( f ` z ) , z } -> ( z e. v <-> z e. { ( f ` z ) , z } ) )
29		eleq2 2504	. . . . . . . . . . . . . . . . . 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 3076	. . . . . . . . . . . . . . . 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 2503	. . . . . . . . . . . . . . . . 17 |- ( w = ( f ` z ) -> ( w e. z <-> ( f ` z ) e. z ) )
34		eleq1 2503	. . . . . . . . . . . . . . . . . . 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 2739	. . . . . . . . . . . . . . . . 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 3067	. . . . . . . . . . . . . . 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 2724	. . . . . . . . . . . . . 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 2978	. . . . . . . . . . . . . . . . . . . 20 |- v e. _V
46		eqeq1 2449	. . . . . . . . . . . . . . . . . . . . . 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 2739	. . . . . . . . . . . . . . . . . . . 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 3109	. . . . . . . . . . . . . . . . . . 19 |- ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } <-> E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) )
50		neeq1 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = u -> ( z =/= (/) <-> u =/= (/) ) )
51		fveq2 5694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z = u -> ( f ` z ) = ( f ` u ) )
52	51	eleq1d 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. z ) )
53		eleq2 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3073	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( f ` u ) e. u ) ) )
57		elirrv 7815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- -. w e. w
58		eleq2 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- w e. _V
62		fvex 5704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f ` u ) e. _V
63		vex 2978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- u e. _V
64	61, 23, 62, 63	prel12 4052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( v = { ( f ` u ) , u } -> ( w e. v <-> w e. { ( f ` u ) , u } ) )
67		eleq2 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2838	. . . . . . . . . . . . . . . . . . 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 1690	. . . . . . . . . . . . . 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 1685	. . . . . . . . . . 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 3141	. . . . . . . . . . 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 2725	. . . . . . . . . 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 2283	. . . . . . . . . 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 2800	. . . . . 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 2978	. . . . . . . . . . . 12 |- f e. _V
105	104	rnex 6515	. . . . . . . . . . 11 |- ran f e. _V
106		p0ex 4482	. . . . . . . . . . 11 |- { (/) } e. _V
107	105, 106	unex 6381	. . . . . . . . . 10 |- ( ran f u. { (/) } ) e. _V
108		vex 2978	. . . . . . . . . 10 |- x e. _V
109	107, 108	unex 6381	. . . . . . . . 9 |- ( ( ran f u. { (/) } ) u. x ) e. _V
110	109	pwex 4478	. . . . . . . 8 |- ~P ( ( ran f u. { (/) } ) u. x ) e. _V
111		ssun1 3522	. . . . . . . . . . . . . . 15 |- ( ran f u. { (/) } ) C_ ( ( ran f u. { (/) } ) u. x )
112		fvrn0 5715	. . . . . . . . . . . . . . 15 |- ( f ` u ) e. ( ran f u. { (/) } )
113	111, 112	sselii 3356	. . . . . . . . . . . . . 14 |- ( f ` u ) e. ( ( ran f u. { (/) } ) u. x )
114		elun2 3527	. . . . . . . . . . . . . 14 |- ( u e. x -> u e. ( ( ran f u. { (/) } ) u. x ) )
115		prssi 4032	. . . . . . . . . . . . . 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 4537	. . . . . . . . . . . . . 14 |- { ( f ` u ) , u } e. _V
118	117	elpw 3869	. . . . . . . . . . . . 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 2503	. . . . . . . . . . . 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 2838	. . . . . . . . 9 |- ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) )
124	123	abssi 3430	. . . . . . . 8 |- { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } C_ ~P ( ( ran f u. { (/) } ) u. x )
125	110, 124	ssexi 4440	. . . . . . 7 |- { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } e. _V
126		rexeq 2921	. . . . . . . . . 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 2908	. . . . . . . . 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 2738	. . . . . . 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 3067	. . . . . 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 1688	. . . 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 1604	. . 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 8302	. 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 1367   = wceq 1369   E.wex 1586   e. wcel 1756   E!weu 2253   E*wmo 2254   {cab 2429   =/= wne 2609   A.wral 2718   E.wrex 2719   E!wreu 2720   u. cun 3329   C_ wss 3331   (/)c0 3640   ~Pcpw 3863   {csn 3880   {cpr 3882   ran crn 4844   ` cfv 5421  CHOICEwac 8288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-reg 7810

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-reu 2725  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-eprel 4635  df-id 4639  df-fr 4682  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-riota 6055  df-ac 8289

This theorem is referenced by:  dfac7  8304