Metamath Proof Explorer

Theorem dfac9

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

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

Proof

Step Hyp Ref Expression
1 dfac3 
 |-  ( CHOICE <-> A. s E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
2 vex 
 |-  f e. _V
3 2 rnex 
 |-  ran f e. _V
4 raleq 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( (/) e/ ran f <-> -. (/) e. ran f )
8 7 biimpi 
 |-  ( (/) e/ ran f -> -. (/) e. ran f )
9 8 ad2antlr 
 |-  ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> -. (/) e. ran f )
10 fvelrn 
 |-  ( ( Fun f /\ x e. dom f ) -> ( f ` x ) e. ran f )
11 10 adantlr 
 |-  ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( f ` x ) e. ran f )
12 eleq1 
 |-  ( ( f ` x ) = (/) -> ( ( f ` x ) e. ran f <-> (/) e. ran f ) )
13 11 12 syl5ibcom 
 |-  ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( ( f ` x ) = (/) -> (/) e. ran f ) )
14 13 necon3bd 
 |-  ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( -. (/) e. ran f -> ( f ` x ) =/= (/) ) )
15 9 14 mpd 
 |-  ( ( ( Fun f /\ (/) e/ ran f ) /\ x e. dom f ) -> ( f ` x ) =/= (/) )
16 15 adantlr 
 |-  ( ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) /\ x e. dom f ) -> ( f ` x ) =/= (/) )
17 neeq1 
 |-  ( t = ( f ` x ) -> ( t =/= (/) <-> ( f ` x ) =/= (/) ) )
18 fveq2 
 |-  ( t = ( f ` x ) -> ( g ` t ) = ( g ` ( f ` x ) ) )
19 id 
 |-  ( t = ( f ` x ) -> t = ( f ` x ) )
20 18 19 eleq12d 
 |-  ( t = ( f ` x ) -> ( ( g ` t ) e. t <-> ( g ` ( f ` x ) ) e. ( f ` x ) ) )
21 17 20 imbi12d 
 |-  ( t = ( f ` x ) -> ( ( t =/= (/) -> ( g ` t ) e. t ) <-> ( ( f ` x ) =/= (/) -> ( g ` ( f ` x ) ) e. ( f ` x ) ) ) )
22 simplr 
 |-  ( ( ( ( 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 ) )
23 10 ad4ant14 
 |-  ( ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) /\ x e. dom f ) -> ( f ` x ) e. ran f )
24 21 22 23 rspcdva 
 |-  ( ( ( ( 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 ) ) )
25 16 24 mpd 
 |-  ( ( ( ( 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 ) )
26 25 ralrimiva 
 |-  ( ( ( 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 ) )
27 2 dmex 
 |-  dom f e. _V
28 mptelixpg 
 |-  ( 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 ) ) )
29 27 28 ax-mp 
 |-  ( ( 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 ) )
30 26 29 sylibr 
 |-  ( ( ( 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 ) )
31 30 ne0d 
 |-  ( ( ( Fun f /\ (/) e/ ran f ) /\ A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) ) -> X_ x e. dom f ( f ` x ) =/= (/) )
32 31 ex 
 |-  ( ( Fun f /\ (/) e/ ran f ) -> ( A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )
33 32 exlimdv 
 |-  ( ( Fun f /\ (/) e/ ran f ) -> ( E. g A. t e. ran f ( t =/= (/) -> ( g ` t ) e. t ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )
34 6 33 syl5com 
 |-  ( 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 ) =/= (/) ) )
35 34 alrimiv 
 |-  ( 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 ) =/= (/) ) )
36 fnresi 
 |-  ( _I |` ( s \ { (/) } ) ) Fn ( s \ { (/) } )
37 fnfun 
 |-  ( ( _I |` ( s \ { (/) } ) ) Fn ( s \ { (/) } ) -> Fun ( _I |` ( s \ { (/) } ) ) )
38 36 37 ax-mp 
 |-  Fun ( _I |` ( s \ { (/) } ) )
39 neldifsn 
 |-  -. (/) e. ( s \ { (/) } )
40 vex 
 |-  s e. _V
41 40 difexi 
 |-  ( s \ { (/) } ) e. _V
42 resiexg 
 |-  ( ( s \ { (/) } ) e. _V -> ( _I |` ( s \ { (/) } ) ) e. _V )
43 41 42 ax-mp 
 |-  ( _I |` ( s \ { (/) } ) ) e. _V
44 funeq 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ( Fun f <-> Fun ( _I |` ( s \ { (/) } ) ) ) )
45 rneq 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ran f = ran ( _I |` ( s \ { (/) } ) ) )
46 rnresi 
 |-  ran ( _I |` ( s \ { (/) } ) ) = ( s \ { (/) } )
47 45 46 eqtrdi 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ran f = ( s \ { (/) } ) )
48 47 eleq2d 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ( (/) e. ran f <-> (/) e. ( s \ { (/) } ) ) )
49 48 notbid 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ( -. (/) e. ran f <-> -. (/) e. ( s \ { (/) } ) ) )
50 7 49 bitrid 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ( (/) e/ ran f <-> -. (/) e. ( s \ { (/) } ) ) )
51 44 50 anbi12d 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ( ( Fun f /\ (/) e/ ran f ) <-> ( Fun ( _I |` ( s \ { (/) } ) ) /\ -. (/) e. ( s \ { (/) } ) ) ) )
52 dmeq 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> dom f = dom ( _I |` ( s \ { (/) } ) ) )
53 dmresi 
 |-  dom ( _I |` ( s \ { (/) } ) ) = ( s \ { (/) } )
54 52 53 eqtrdi 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> dom f = ( s \ { (/) } ) )
55 54 ixpeq1d 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> X_ x e. dom f ( f ` x ) = X_ x e. ( s \ { (/) } ) ( f ` x ) )
56 fveq1 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ( f ` x ) = ( ( _I |` ( s \ { (/) } ) ) ` x ) )
57 fvresi 
 |-  ( x e. ( s \ { (/) } ) -> ( ( _I |` ( s \ { (/) } ) ) ` x ) = x )
58 56 57 sylan9eq 
 |-  ( ( f = ( _I |` ( s \ { (/) } ) ) /\ x e. ( s \ { (/) } ) ) -> ( f ` x ) = x )
59 58 ixpeq2dva 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> X_ x e. ( s \ { (/) } ) ( f ` x ) = X_ x e. ( s \ { (/) } ) x )
60 55 59 eqtrd 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> X_ x e. dom f ( f ` x ) = X_ x e. ( s \ { (/) } ) x )
61 60 neeq1d 
 |-  ( f = ( _I |` ( s \ { (/) } ) ) -> ( X_ x e. dom f ( f ` x ) =/= (/) <-> X_ x e. ( s \ { (/) } ) x =/= (/) ) )
62 51 61 imbi12d 
 |-  ( 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 =/= (/) ) ) )
63 43 62 spcv 
 |-  ( A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) -> ( ( Fun ( _I |` ( s \ { (/) } ) ) /\ -. (/) e. ( s \ { (/) } ) ) -> X_ x e. ( s \ { (/) } ) x =/= (/) ) )
64 38 39 63 mp2ani 
 |-  ( A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) -> X_ x e. ( s \ { (/) } ) x =/= (/) )
65 n0 
 |-  ( X_ x e. ( s \ { (/) } ) x =/= (/) <-> E. g g e. X_ x e. ( s \ { (/) } ) x )
66 vex 
 |-  g e. _V
67 66 elixp 
 |-  ( g e. X_ x e. ( s \ { (/) } ) x <-> ( g Fn ( s \ { (/) } ) /\ A. x e. ( s \ { (/) } ) ( g ` x ) e. x ) )
68 eldifsn 
 |-  ( x e. ( s \ { (/) } ) <-> ( x e. s /\ x =/= (/) ) )
69 68 imbi1i 
 |-  ( ( x e. ( s \ { (/) } ) -> ( g ` x ) e. x ) <-> ( ( x e. s /\ x =/= (/) ) -> ( g ` x ) e. x ) )
70 impexp 
 |-  ( ( ( x e. s /\ x =/= (/) ) -> ( g ` x ) e. x ) <-> ( x e. s -> ( x =/= (/) -> ( g ` x ) e. x ) ) )
71 69 70 bitri 
 |-  ( ( x e. ( s \ { (/) } ) -> ( g ` x ) e. x ) <-> ( x e. s -> ( x =/= (/) -> ( g ` x ) e. x ) ) )
72 71 ralbii2 
 |-  ( A. x e. ( s \ { (/) } ) ( g ` x ) e. x <-> A. x e. s ( x =/= (/) -> ( g ` x ) e. x ) )
73 neeq1 
 |-  ( x = t -> ( x =/= (/) <-> t =/= (/) ) )
74 fveq2 
 |-  ( x = t -> ( g ` x ) = ( g ` t ) )
75 id 
 |-  ( x = t -> x = t )
76 74 75 eleq12d 
 |-  ( x = t -> ( ( g ` x ) e. x <-> ( g ` t ) e. t ) )
77 73 76 imbi12d 
 |-  ( x = t -> ( ( x =/= (/) -> ( g ` x ) e. x ) <-> ( t =/= (/) -> ( g ` t ) e. t ) ) )
78 77 cbvralvw 
 |-  ( A. x e. s ( x =/= (/) -> ( g ` x ) e. x ) <-> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
79 72 78 bitri 
 |-  ( A. x e. ( s \ { (/) } ) ( g ` x ) e. x <-> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
80 79 biimpi 
 |-  ( A. x e. ( s \ { (/) } ) ( g ` x ) e. x -> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
81 67 80 simplbiim 
 |-  ( g e. X_ x e. ( s \ { (/) } ) x -> A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
82 81 eximi 
 |-  ( E. g g e. X_ x e. ( s \ { (/) } ) x -> E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
83 65 82 sylbi 
 |-  ( X_ x e. ( s \ { (/) } ) x =/= (/) -> E. g A. t e. s ( t =/= (/) -> ( g ` t ) e. t ) )
84 64 83 syl 
 |-  ( 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 ) )
85 84 alrimiv 
 |-  ( 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 ) )
86 35 85 impbii 
 |-  ( 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 ) =/= (/) ) )
87 1 86 bitri 
 |-  ( CHOICE <-> A. f ( ( Fun f /\ (/) e/ ran f ) -> X_ x e. dom f ( f ` x ) =/= (/) ) )