Theorem dfac2 8514

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8845). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 8026 and preleq 8037 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 8513.) 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 8505	. . 3 |- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
2		nfra1 2824	. . . . . . 7 |- F/ z A. z e. x ( z =/= (/) -> ( f ` z ) e. z )
3		rsp 2809	. . . . . . . . . . . . 13 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> ( f ` z ) e. z ) ) )
4		equid 1777	. . . . . . . . . . . . . . . . . . 19 |- z = z
5		neeq1 2724	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
6		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> ( u = z <-> z = z ) )
7	5, 6	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 |- ( u = z -> ( ( u =/= (/) /\ u = z ) <-> ( z =/= (/) /\ z = z ) ) )
8	7	rspcev 3196	. . . . . . . . . . . . . . . . . . 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 5856	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = z -> ( f ` u ) = ( f ` z ) )
11	10	preq1d 4100	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` u ) , u } = { ( f ` z ) , u } )
12		preq2 4095	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = z -> { ( f ` z ) , u } = { ( f ` z ) , z } )
13	11, 12	eqtr2d 2485	. . . . . . . . . . . . . . . . . . . 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 2911	. . . . . . . . . . . . . . . . . 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 2447	. . . . . . . . . . . . . . . . . . . 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 2954	. . . . . . . . . . . . . . . . . 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 3232	. . . . . . . . . . . . . . . . 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 3098	. . . . . . . . . . . . . . . . . 18 |- z e. _V
24	23	prid2 4124	. . . . . . . . . . . . . . . . 17 |- z e. { ( f ` z ) , z }
25		fvex 5866	. . . . . . . . . . . . . . . . . 18 |- ( f ` z ) e. _V
26	25	prid1 4123	. . . . . . . . . . . . . . . . 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 2516	. . . . . . . . . . . . . . . . . 18 |- ( v = { ( f ` z ) , z } -> ( z e. v <-> z e. { ( f ` z ) , z } ) )
29		eleq2 2516	. . . . . . . . . . . . . . . . . 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 3196	. . . . . . . . . . . . . . . 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 2515	. . . . . . . . . . . . . . . . 17 |- ( w = ( f ` z ) -> ( w e. z <-> ( f ` z ) e. z ) )
34		eleq1 2515	. . . . . . . . . . . . . . . . . . 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 2954	. . . . . . . . . . . . . . . . 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 3187	. . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . 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 3098	. . . . . . . . . . . . . . . . . . . 20 |- v e. _V
46		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . 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 2954	. . . . . . . . . . . . . . . . . . . 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 3232	. . . . . . . . . . . . . . . . . . 19 |- ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } <-> E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) )
50		neeq1 2724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = u -> ( z =/= (/) <-> u =/= (/) ) )
51		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z = u -> ( f ` z ) = ( f ` u ) )
52	51	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. z ) )
53		eleq2 2516	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3193	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( f ` u ) e. u ) ) )
57		elirrv 8026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- -. w e. w
58		eleq2 2516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- w e. _V
62		fvex 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( f ` u ) e. _V
63		vex 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- u e. _V
64	61, 23, 62, 63	prel12 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( v = { ( f ` u ) , u } -> ( w e. v <-> w e. { ( f ` u ) , u } ) )
67		eleq2 2516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2929	. . . . . . . . . . . . . . . . . . 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 1711	. . . . . . . . . . . . . 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 1706	. . . . . . . . . . 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 3264	. . . . . . . . . . 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 2800	. . . . . . . . . 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 2296	. . . . . . . . . 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 2843	. . . . . 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 3098	. . . . . . . . . . . 12 |- f e. _V
105	104	rnex 6719	. . . . . . . . . . 11 |- ran f e. _V
106		p0ex 4624	. . . . . . . . . . 11 |- { (/) } e. _V
107	105, 106	unex 6583	. . . . . . . . . 10 |- ( ran f u. { (/) } ) e. _V
108		vex 3098	. . . . . . . . . 10 |- x e. _V
109	107, 108	unex 6583	. . . . . . . . 9 |- ( ( ran f u. { (/) } ) u. x ) e. _V
110	109	pwex 4620	. . . . . . . 8 |- ~P ( ( ran f u. { (/) } ) u. x ) e. _V
111		ssun1 3652	. . . . . . . . . . . . . . 15 |- ( ran f u. { (/) } ) C_ ( ( ran f u. { (/) } ) u. x )
112		fvrn0 5878	. . . . . . . . . . . . . . 15 |- ( f ` u ) e. ( ran f u. { (/) } )
113	111, 112	sselii 3486	. . . . . . . . . . . . . 14 |- ( f ` u ) e. ( ( ran f u. { (/) } ) u. x )
114		elun2 3657	. . . . . . . . . . . . . 14 |- ( u e. x -> u e. ( ( ran f u. { (/) } ) u. x ) )
115		prssi 4171	. . . . . . . . . . . . . 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 4679	. . . . . . . . . . . . . 14 |- { ( f ` u ) , u } e. _V
118	117	elpw 4003	. . . . . . . . . . . . 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 2515	. . . . . . . . . . . 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 2929	. . . . . . . . 9 |- ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) )
124	123	abssi 3560	. . . . . . . 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 3041	. . . . . . . . . 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 3028	. . . . . . . . 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 2882	. . . . . . 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 3187	. . . . . 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 1709	. . . 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 1620	. . 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 8513	. 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 1381   = wceq 1383   E.wex 1599   e. wcel 1804   E!weu 2268   E*wmo 2269   {cab 2428   =/= wne 2638   A.wral 2793   E.wrex 2794   E!wreu 2795   u. cun 3459   C_ wss 3461   (/)c0 3770   ~Pcpw 3997   {csn 4014   {cpr 4016   ran crn 4990   ` cfv 5578  CHOICEwac 8499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-reg 8021

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-eprel 4781  df-id 4785  df-fr 4828  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-riota 6242  df-ac 8500

This theorem is referenced by:  dfac7  8515