Theorem dfac9 8958

Description: Equivalence of the axiom of choice with a statement related to ac9 9305; definition AC3 of [Schechter] p. 139. (Contributed by Stefan O'Rear, 22-Feb-2015.)

Assertion

Ref	Expression
dfac9	|- (CHOICE <-> A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )

Distinct variable group:   x, f

Proof of Theorem dfac9

Dummy variables g s t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfac3 8944	. 2 |- (CHOICE <-> A. s E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
2		vex 3203	. . . . . . 7 |- f e. _V
3	2	rnex 7100	. . . . . 6 |- ran f e. _V
4		raleq 3138	. . . . . . 7 |- ( s = ran f -> ( A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) <-> A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) )
5	4	exbidv 1850	. . . . . 6 |- ( s = ran f -> ( E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) <-> E. g A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) )
6	3, 5	spcv 3299	. . . . 5 |- ( A. s E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) -> E. g A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) )
7		df-nel 2898	. . . . . . . . . . . . . . 15 |- ( (/) e/ ran f <-> -. (/) e. ran f )
8	7	biimpi 206	. . . . . . . . . . . . . 14 |- ( (/) e/ ran f -> -. (/) e. ran f )
9	8	ad2antlr 763	. . . . . . . . . . . . 13 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> -. (/) e. ran f )
10		fvelrn 6352	. . . . . . . . . . . . . . . 16 |- ( ( Fun f /\ x e. dom f ) -> ( f ` x ) e. ran f )
11	10	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( f ` x ) e. ran f )
12		eleq1 2689	. . . . . . . . . . . . . . 15 |- ( ( f ` x ) = (/) -> ( ( f ` x ) e. ran f <-> (/) e. ran f ) )
13	11, 12	syl5ibcom 235	. . . . . . . . . . . . . 14 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( ( f ` x ) = (/) -> (/) e. ran f ) )
14	13	necon3bd 2808	. . . . . . . . . . . . 13 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( -. (/) e. ran f -> ( f ` x ) =/= (/) ) )
15	9, 14	mpd 15	. . . . . . . . . . . 12 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( f ` x ) =/= (/) )
16	15	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) /\ x e. dom f ) -> ( f ` x ) =/= (/) )
17		simpll 790	. . . . . . . . . . . . 13 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) -> Fun f )
18	17, 10	sylan 488	. . . . . . . . . . . 12 |- ( ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) /\ x e. dom f ) -> ( f ` x ) e. ran f )
19		simplr 792	. . . . . . . . . . . 12 |- ( ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) /\ x e. dom f ) -> A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) )
20		neeq1 2856	. . . . . . . . . . . . . 14 |- ( t = ( f ` x ) -> ( t =/= (/) <-> ( f ` x ) =/= (/) ) )
21		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( t = ( f ` x ) -> ( g ` t ) = ( g ` ( f ` x ) ) )
22		id 22	. . . . . . . . . . . . . . 15 |- ( t = ( f ` x ) -> t = ( f ` x ) )
23	21, 22	eleq12d 2695	. . . . . . . . . . . . . 14 |- ( t = ( f ` x ) -> ( ( g ` t ) e. t <-> ( g ` ( f ` x ) ) e. ( f ` x ) ) )
24	20, 23	imbi12d 334	. . . . . . . . . . . . 13 |- ( t = ( f ` x ) -> ( ( t =/= (/) -> ( g ` t ) e. t ) <-> ( ( f ` x ) =/= (/) -> ( g ` ( f ` x ) ) e. ( f ` x ) ) ) )
25	24	rspcva 3307	. . . . . . . . . . . 12 |- ( ( ( f ` x ) e. ran f /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) -> ( ( f ` x ) =/= (/) -> ( g ` ( f ` x ) ) e. ( f ` x ) ) )
26	18, 19, 25	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) /\ x e. dom f ) -> ( ( f ` x ) =/= (/) -> ( g ` ( f ` x ) ) e. ( f ` x ) ) )
27	16, 26	mpd 15	. . . . . . . . . 10 |- ( ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) /\ x e. dom f ) -> ( g ` ( f ` x ) ) e. ( f ` x ) )
28	27	ralrimiva 2966	. . . . . . . . 9 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) -> A. x e. dom f ( g ` ( f ` x ) ) e. ( f ` x ) )
29	2	dmex 7099	. . . . . . . . . 10 |- dom f e. _V
30		mptelixpg 7945	. . . . . . . . . 10 |- ( dom f e. _V -> ( ( x e. dom f |-> ( g ` ( f ` x ) ) ) e. X_ x e. dom f ( f ` x ) <-> A. x e. dom f ( g ` ( f ` x ) ) e. ( f ` x ) ) )
31	29, 30	ax-mp 5	. . . . . . . . 9 |- ( ( x e. dom f |-> ( g ` ( f ` x ) ) ) e. X_ x e. dom f ( f ` x ) <-> A. x e. dom f ( g ` ( f ` x ) ) e. ( f ` x ) )
32	28, 31	sylibr 224	. . . . . . . 8 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) -> ( x e. dom f |-> ( g ` ( f ` x ) ) ) e. X_ x e. dom f ( f ` x ) )
33		ne0i 3921	. . . . . . . 8 |- ( ( x e. dom f |-> ( g ` ( f ` x ) ) ) e. X_ x e. dom f ( f ` x ) -> X_ x e. dom f ( f ` x ) =/= (/) )
34	32, 33	syl 17	. . . . . . 7 |- ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) -> X_ x e. dom f ( f ` x ) =/= (/) )
35	34	ex 450	. . . . . 6 |- ( ( Fun f /\ (/) e/ ran f ) -> ( A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )
36	35	exlimdv 1861	. . . . 5 |- ( ( Fun f /\ (/) e/ ran f ) -> ( E. g A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )
37	6, 36	syl5com 31	. . . 4 |- ( A. s E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) -> ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )
38	37	alrimiv 1855	. . 3 |- ( A. s E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) -> A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )
39		fnresi 6008	. . . . . . 7 |- ( _I |` ( s \ { (/) } ) ) Fn ( s \ { (/) } )
40		fnfun 5988	. . . . . . 7 |- ( ( _I |` ( s \ { (/) } ) ) Fn ( s \ { (/) } ) -> Fun ( _I |` ( s \ { (/) } ) ) )
41	39, 40	ax-mp 5	. . . . . 6 |- Fun ( _I |` ( s \ { (/) } ) )
42		neldifsn 4321	. . . . . 6 |- -. (/) e. ( s \ { (/) } )
43		vex 3203	. . . . . . . . 9 |- s e. _V
44		difexg 4808	. . . . . . . . 9 |- ( s e. _V -> ( s \ { (/) } ) e. _V )
45	43, 44	ax-mp 5	. . . . . . . 8 |- ( s \ { (/) } ) e. _V
46		resiexg 7102	. . . . . . . 8 |- ( ( s \ { (/) } ) e. _V -> ( _I |` ( s \ { (/) } ) ) e. _V )
47	45, 46	ax-mp 5	. . . . . . 7 |- ( _I |` ( s \ { (/) } ) ) e. _V
48		funeq 5908	. . . . . . . . 9 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( Fun f <-> Fun ( _I |` ( s \ { (/) } ) ) ) )
49		rneq 5351	. . . . . . . . . . . . 13 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ran f = ran ( _I |` ( s \ { (/) } ) ) )
50		rnresi 5479	. . . . . . . . . . . . 13 |- ran ( _I |` ( s \ { (/) } ) ) = ( s \ { (/) } )
51	49, 50	syl6eq 2672	. . . . . . . . . . . 12 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ran f = ( s \ { (/) } ) )
52	51	eleq2d 2687	. . . . . . . . . . 11 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( (/) e. ran f <-> (/) e. ( s \ { (/) } ) ) )
53	52	notbid 308	. . . . . . . . . 10 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( -. (/) e. ran f <-> -. (/) e. ( s \ { (/) } ) ) )
54	7, 53	syl5bb 272	. . . . . . . . 9 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( (/) e/ ran f <-> -. (/) e. ( s \ { (/) } ) ) )
55	48, 54	anbi12d 747	. . . . . . . 8 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( ( Fun f /\ (/) e/ ran f ) <-> ( Fun ( _I |` ( s \ { (/) } ) ) /\ -. (/) e. ( s \ { (/) } ) ) ) )
56		dmeq 5324	. . . . . . . . . . . 12 |- ( f = ( _I |` ( s \ { (/) } ) ) -> dom f = dom ( _I |` ( s \ { (/) } ) ) )
57		dmresi 5457	. . . . . . . . . . . 12 |- dom ( _I |` ( s \ { (/) } ) ) = ( s \ { (/) } )
58	56, 57	syl6eq 2672	. . . . . . . . . . 11 |- ( f = ( _I |` ( s \ { (/) } ) ) -> dom f = ( s \ { (/) } ) )
59	58	ixpeq1d 7920	. . . . . . . . . 10 |- ( f = ( _I |` ( s \ { (/) } ) ) -> X_ x e. dom f ( f ` x ) = X_ x e. ( s \ { (/) } ) ( f ` x ) )
60		fveq1 6190	. . . . . . . . . . . 12 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( f ` x ) = ( ( _I |` ( s \ { (/) } ) ) ` x ) )
61		fvresi 6439	. . . . . . . . . . . 12 |- ( x e. ( s \ { (/) } ) -> ( ( _I |` ( s \ { (/) } ) ) ` x ) = x )
62	60, 61	sylan9eq 2676	. . . . . . . . . . 11 |- ( ( f = ( _I |` ( s \ { (/) } ) ) /\ x e. ( s \ { (/) } ) ) -> ( f ` x ) = x )
63	62	ixpeq2dva 7923	. . . . . . . . . 10 |- ( f = ( _I |` ( s \ { (/) } ) ) -> X_ x e. ( s \ { (/) } ) ( f ` x ) = X_ x e. ( s \ { (/) } ) x )
64	59, 63	eqtrd 2656	. . . . . . . . 9 |- ( f = ( _I |` ( s \ { (/) } ) ) -> X_ x e. dom f ( f ` x ) = X_ x e. ( s \ { (/) } ) x )
65	64	neeq1d 2853	. . . . . . . 8 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( X_ x e. dom f ( f ` x ) =/= (/) <-> X_ x e. ( s \ { (/) } ) x =/= (/) ) )
66	55, 65	imbi12d 334	. . . . . . 7 |- ( f = ( _I |` ( s \ { (/) } ) ) -> ( ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) <-> ( ( Fun ( _I |` ( s \ { (/) } ) ) /\ -. (/) e. ( s \ { (/) } ) ) -> X_ x e. ( s \ { (/) } ) x =/= (/) ) ) )
67	47, 66	spcv 3299	. . . . . 6 |- ( A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) -> ( ( Fun ( _I |` ( s \ { (/) } ) ) /\ -. (/) e. ( s \ { (/) } ) ) -> X_ x e. ( s \ { (/) } ) x =/= (/) ) )
68	41, 42, 67	mp2ani 714	. . . . 5 |- ( A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) -> X_ x e. ( s \ { (/) } ) x =/= (/) )
69		n0 3931	. . . . . 6 |- ( X_ x e. ( s \ { (/) } ) x =/= (/) <-> E. g g e. X_ x e. ( s \ { (/) } ) x )
70		vex 3203	. . . . . . . . 9 |- g e. _V
71	70	elixp 7915	. . . . . . . 8 |- ( g e. X_ x e. ( s \ { (/) } ) x <-> ( g Fn ( s \ { (/) } ) /\ A. x e. ( s \ { (/) } ) ( g ` x ) e. x ) )
72		eldifsn 4317	. . . . . . . . . . . . . 14 |- ( x e. ( s \ { (/) } ) <-> ( x e. s /\ x =/= (/) ) )
73	72	imbi1i 339	. . . . . . . . . . . . 13 |- ( ( x e. ( s \ { (/) } ) -> ( g ` x ) e. x ) <-> ( ( x e. s /\ x =/= (/) ) -> ( g ` x ) e. x ) )
74		impexp 462	. . . . . . . . . . . . 13 |- ( ( ( x e. s /\ x =/= (/) ) -> ( g ` x ) e. x ) <-> ( x e. s -> ( x =/= (/) -> ( g ` x ) e. x ) ) )
75	73, 74	bitri 264	. . . . . . . . . . . 12 |- ( ( x e. ( s \ { (/) } ) -> ( g ` x ) e. x ) <-> ( x e. s -> ( x =/= (/) -> ( g ` x ) e. x ) ) )
76	75	ralbii2 2978	. . . . . . . . . . 11 |- ( A. x e. ( s \ { (/) } ) ( g ` x ) e. x <-> A. x e. s ( x =/= (/) -> ( g ` x ) e. x ) )
77		neeq1 2856	. . . . . . . . . . . . 13 |- ( x = t -> ( x =/= (/) <-> t =/= (/) ) )
78		fveq2 6191	. . . . . . . . . . . . . 14 |- ( x = t -> ( g ` x ) = ( g ` t ) )
79		id 22	. . . . . . . . . . . . . 14 |- ( x = t -> x = t )
80	78, 79	eleq12d 2695	. . . . . . . . . . . . 13 |- ( x = t -> ( ( g ` x ) e. x <-> ( g ` t ) e. t ) )
81	77, 80	imbi12d 334	. . . . . . . . . . . 12 |- ( x = t -> ( ( x =/= (/) -> ( g ` x ) e. x ) <-> ( t =/= (/) -> ( g ` t ) e. t ) ) )
82	81	cbvralv 3171	. . . . . . . . . . 11 |- ( A. x e. s ( x =/= (/) -> ( g ` x ) e. x ) <-> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
83	76, 82	bitri 264	. . . . . . . . . 10 |- ( A. x e. ( s \ { (/) } ) ( g ` x ) e. x <-> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
84	83	biimpi 206	. . . . . . . . 9 |- ( A. x e. ( s \ { (/) } ) ( g ` x ) e. x -> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
85	84	adantl 482	. . . . . . . 8 |- ( ( g Fn ( s \ { (/) } ) /\ A. x e. ( s \ { (/) } ) ( g ` x ) e. x ) -> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
86	71, 85	sylbi 207	. . . . . . 7 |- ( g e. X_ x e. ( s \ { (/) } ) x -> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
87	86	eximi 1762	. . . . . 6 |- ( E. g g e. X_ x e. ( s \ { (/) } ) x -> E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
88	69, 87	sylbi 207	. . . . 5 |- ( X_ x e. ( s \ { (/) } ) x =/= (/) -> E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
89	68, 88	syl 17	. . . 4 |- ( A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) -> E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
90	89	alrimiv 1855	. . 3 |- ( A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) -> A. s E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
91	38, 90	impbii 199	. 2 |- ( A. s E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) <-> A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )
92	1, 91	bitri 264	1 |- (CHOICE <-> A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   e/ wnel 2897   A.wral 2912   _Vcvv 3200   \ cdif 3571   (/)c0 3915   {csn 4177   |-> cmpt 4729   _I cid 5023   dom cdm 5114   ran crn 5115   |` cres 5116   Fun wfun 5882   Fn wfn 5883   ` cfv 5888   X_cixp 7908  CHOICEwac 8938

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

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

This theorem is referenced by:  dfac14  21421  dfac21  37636