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 f Fun f ran f x dom f f x

Proof

Step Hyp Ref Expression
1 dfac3 CHOICE s g t s t g t t
2 vex f V
3 2 rnex ran f V
4 raleq s = ran f t s t g t t t ran f t g t t
5 4 exbidv s = ran f g t s t g t t g t ran f t g t t
6 3 5 spcv s g t s t g t t g t ran f t g t t
7 df-nel ran f ¬ ran f
8 7 biimpi ran f ¬ ran f
9 8 ad2antlr Fun f ran f x dom f ¬ ran f
10 fvelrn Fun f x dom f f x ran f
11 10 adantlr Fun f ran f x dom f f x ran f
12 eleq1 f x = f x ran f ran f
13 11 12 syl5ibcom Fun f ran f x dom f f x = ran f
14 13 necon3bd Fun f ran f x dom f ¬ ran f f x
15 9 14 mpd Fun f ran f x dom f f x
16 15 adantlr Fun f ran f t ran f t g t t x 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 t g f x f x
21 17 20 imbi12d t = f x t g t t f x g f x f x
22 simplr Fun f ran f t ran f t g t t x dom f t ran f t g t t
23 10 ad4ant14 Fun f ran f t ran f t g t t x dom f f x ran f
24 21 22 23 rspcdva Fun f ran f t ran f t g t t x dom f f x g f x f x
25 16 24 mpd Fun f ran f t ran f t g t t x dom f g f x f x
26 25 ralrimiva Fun f ran f t ran f t g t t x dom f g f x f x
27 2 dmex dom f V
28 mptelixpg dom f V x dom f g f x x dom f f x x dom f g f x f x
29 27 28 ax-mp x dom f g f x x dom f f x x dom f g f x f x
30 26 29 sylibr Fun f ran f t ran f t g t t x dom f g f x x dom f f x
31 30 ne0d Fun f ran f t ran f t g t t x dom f f x
32 31 ex Fun f ran f t ran f t g t t x dom f f x
33 32 exlimdv Fun f ran f g t ran f t g t t x dom f f x
34 6 33 syl5com s g t s t g t t Fun f ran f x dom f f x
35 34 alrimiv s g t s t g t t f Fun f ran f x 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 ¬ s
40 vex s V
41 40 difexi s V
42 resiexg s V I s V
43 41 42 ax-mp I s 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 ran f s
49 48 notbid f = I s ¬ ran f ¬ s
50 7 49 syl5bb f = I s ran f ¬ s
51 44 50 anbi12d f = I s Fun f ran f Fun I s ¬ 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 dom f f x = x s f x
56 fveq1 f = I s f x = I s x
57 fvresi x s I s x = x
58 56 57 sylan9eq f = I s x s f x = x
59 58 ixpeq2dva f = I s x s f x = x s x
60 55 59 eqtrd f = I s x dom f f x = x s x
61 60 neeq1d f = I s x dom f f x x s x
62 51 61 imbi12d f = I s Fun f ran f x dom f f x Fun I s ¬ s x s x
63 43 62 spcv f Fun f ran f x dom f f x Fun I s ¬ s x s x
64 38 39 63 mp2ani f Fun f ran f x dom f f x x s x
65 n0 x s x g g x s x
66 vex g V
67 66 elixp g x s x g Fn s x s g x x
68 eldifsn x s x s x
69 68 imbi1i x s g x x x s x g x x
70 impexp x s x g x x x s x g x x
71 69 70 bitri x s g x x x s x g x x
72 71 ralbii2 x s g x x x s x g x 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 x g t t
77 73 76 imbi12d x = t x g x x t g t t
78 77 cbvralvw x s x g x x t s t g t t
79 72 78 bitri x s g x x t s t g t t
80 79 biimpi x s g x x t s t g t t
81 67 80 simplbiim g x s x t s t g t t
82 81 eximi g g x s x g t s t g t t
83 65 82 sylbi x s x g t s t g t t
84 64 83 syl f Fun f ran f x dom f f x g t s t g t t
85 84 alrimiv f Fun f ran f x dom f f x s g t s t g t t
86 35 85 impbii s g t s t g t t f Fun f ran f x dom f f x
87 1 86 bitri CHOICE f Fun f ran f x dom f f x