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↔∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅

Proof

Step Hyp Ref Expression
1 dfac3 ⊢CHOICE↔∀s∃g∀t∈st≠∅→g⁡t∈t
2 vex ⊢f∈V
3 2 rnex ⊢ran⁡f∈V
4 raleq ⊢s=ran⁡f→∀t∈st≠∅→g⁡t∈t↔∀t∈ran⁡ft≠∅→g⁡t∈t
5 4 exbidv ⊢s=ran⁡f→∃g∀t∈st≠∅→g⁡t∈t↔∃g∀t∈ran⁡ft≠∅→g⁡t∈t
6 3 5 spcv ⊢∀s∃g∀t∈st≠∅→g⁡t∈t→∃g∀t∈ran⁡ft≠∅→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⁡ft≠∅→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⁡ft≠∅→g⁡t∈t∧x∈dom⁡f→∀t∈ran⁡ft≠∅→g⁡t∈t
23 10 ad4ant14 ⊢Fun⁡f∧∅∉ran⁡f∧∀t∈ran⁡ft≠∅→g⁡t∈t∧x∈dom⁡f→f⁡x∈ran⁡f
24 21 22 23 rspcdva ⊢Fun⁡f∧∅∉ran⁡f∧∀t∈ran⁡ft≠∅→g⁡t∈t∧x∈dom⁡f→f⁡x≠∅→g⁡f⁡x∈f⁡x
25 16 24 mpd ⊢Fun⁡f∧∅∉ran⁡f∧∀t∈ran⁡ft≠∅→g⁡t∈t∧x∈dom⁡f→g⁡f⁡x∈f⁡x
26 25 ralrimiva ⊢Fun⁡f∧∅∉ran⁡f∧∀t∈ran⁡ft≠∅→g⁡t∈t→∀x∈dom⁡fg⁡f⁡x∈f⁡x
27 2 dmex ⊢dom⁡f∈V
28 mptelixpg ⊢dom⁡f∈V→x∈dom⁡f⟼g⁡f⁡x∈⨉x∈dom⁡ff⁡x↔∀x∈dom⁡fg⁡f⁡x∈f⁡x
29 27 28 ax-mp ⊢x∈dom⁡f⟼g⁡f⁡x∈⨉x∈dom⁡ff⁡x↔∀x∈dom⁡fg⁡f⁡x∈f⁡x
30 26 29 sylibr ⊢Fun⁡f∧∅∉ran⁡f∧∀t∈ran⁡ft≠∅→g⁡t∈t→x∈dom⁡f⟼g⁡f⁡x∈⨉x∈dom⁡ff⁡x
31 30 ne0d ⊢Fun⁡f∧∅∉ran⁡f∧∀t∈ran⁡ft≠∅→g⁡t∈t→⨉x∈dom⁡ff⁡x≠∅
32 31 ex ⊢Fun⁡f∧∅∉ran⁡f→∀t∈ran⁡ft≠∅→g⁡t∈t→⨉x∈dom⁡ff⁡x≠∅
33 32 exlimdv ⊢Fun⁡f∧∅∉ran⁡f→∃g∀t∈ran⁡ft≠∅→g⁡t∈t→⨉x∈dom⁡ff⁡x≠∅
34 6 33 syl5com ⊢∀s∃g∀t∈st≠∅→g⁡t∈t→Fun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅
35 34 alrimiv ⊢∀s∃g∀t∈st≠∅→g⁡t∈t→∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅
36 fnresi ⊢I↾s∖∅Fns∖∅
37 fnfun ⊢I↾s∖∅Fns∖∅→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 bitrid ⊢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⁡ff⁡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⁡ff⁡x=⨉x∈s∖∅x
61 60 neeq1d ⊢f=I↾s∖∅→⨉x∈dom⁡ff⁡x≠∅↔⨉x∈s∖∅x≠∅
62 51 61 imbi12d ⊢f=I↾s∖∅→Fun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅↔Fun⁡I↾s∖∅∧¬∅∈s∖∅→⨉x∈s∖∅x≠∅
63 43 62 spcv ⊢∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅→Fun⁡I↾s∖∅∧¬∅∈s∖∅→⨉x∈s∖∅x≠∅
64 38 39 63 mp2ani ⊢∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅→⨉x∈s∖∅x≠∅
65 n0 ⊢⨉x∈s∖∅x≠∅↔∃gg∈⨉x∈s∖∅x
66 vex ⊢g∈V
67 66 elixp ⊢g∈⨉x∈s∖∅x↔gFns∖∅∧∀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∈sx≠∅→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∈sx≠∅→g⁡x∈x↔∀t∈st≠∅→g⁡t∈t
79 72 78 bitri ⊢∀x∈s∖∅g⁡x∈x↔∀t∈st≠∅→g⁡t∈t
80 79 biimpi ⊢∀x∈s∖∅g⁡x∈x→∀t∈st≠∅→g⁡t∈t
81 67 80 simplbiim ⊢g∈⨉x∈s∖∅x→∀t∈st≠∅→g⁡t∈t
82 81 eximi ⊢∃gg∈⨉x∈s∖∅x→∃g∀t∈st≠∅→g⁡t∈t
83 65 82 sylbi ⊢⨉x∈s∖∅x≠∅→∃g∀t∈st≠∅→g⁡t∈t
84 64 83 syl ⊢∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅→∃g∀t∈st≠∅→g⁡t∈t
85 84 alrimiv ⊢∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅→∀s∃g∀t∈st≠∅→g⁡t∈t
86 35 85 impbii ⊢∀s∃g∀t∈st≠∅→g⁡t∈t↔∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅
87 1 86 bitri ⊢CHOICE↔∀fFun⁡f∧∅∉ran⁡f→⨉x∈dom⁡ff⁡x≠∅