Metamath Proof Explorer

Theorem acnnum

Description: A set X which has choice sequences on it of length ~P X is well-orderable (and hence has choice sequences of every length). (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acnnum ⊢X∈AC_𝒫X↔X∈dom⁡card

Proof

Step Hyp Ref Expression
1 pwexg ⊢X∈AC_𝒫X→𝒫X∈V
2 difss ⊢𝒫X∖∅⊆𝒫X
3 ssdomg ⊢𝒫X∈V→𝒫X∖∅⊆𝒫X→𝒫X∖∅≼𝒫X
4 1 2 3 mpisyl ⊢X∈AC_𝒫X→𝒫X∖∅≼𝒫X
5 acndom ⊢𝒫X∖∅≼𝒫X→X∈AC_𝒫X→X∈AC_𝒫X∖∅
6 4 5 mpcom ⊢X∈AC_𝒫X→X∈AC_𝒫X∖∅
7 eldifsn ⊢x∈𝒫X∖∅↔x∈𝒫X∧x≠∅
8 elpwi ⊢x∈𝒫X→x⊆X
9 8 anim1i ⊢x∈𝒫X∧x≠∅→x⊆X∧x≠∅
10 7 9 sylbi ⊢x∈𝒫X∖∅→x⊆X∧x≠∅
11 10 rgen ⊢∀x∈𝒫X∖∅x⊆X∧x≠∅
12 acni2 ⊢X∈AC_𝒫X∖∅∧∀x∈𝒫X∖∅x⊆X∧x≠∅→∃ff:𝒫X∖∅⟶X∧∀x∈𝒫X∖∅f⁡x∈x
13 6 11 12 sylancl ⊢X∈AC_𝒫X→∃ff:𝒫X∖∅⟶X∧∀x∈𝒫X∖∅f⁡x∈x
14 simpr ⊢f:𝒫X∖∅⟶X∧∀x∈𝒫X∖∅f⁡x∈x→∀x∈𝒫X∖∅f⁡x∈x
15 7 imbi1i ⊢x∈𝒫X∖∅→f⁡x∈x↔x∈𝒫X∧x≠∅→f⁡x∈x
16 impexp ⊢x∈𝒫X∧x≠∅→f⁡x∈x↔x∈𝒫X→x≠∅→f⁡x∈x
17 15 16 bitri ⊢x∈𝒫X∖∅→f⁡x∈x↔x∈𝒫X→x≠∅→f⁡x∈x
18 17 ralbii2 ⊢∀x∈𝒫X∖∅f⁡x∈x↔∀x∈𝒫Xx≠∅→f⁡x∈x
19 14 18 sylib ⊢f:𝒫X∖∅⟶X∧∀x∈𝒫X∖∅f⁡x∈x→∀x∈𝒫Xx≠∅→f⁡x∈x
20 19 eximi ⊢∃ff:𝒫X∖∅⟶X∧∀x∈𝒫X∖∅f⁡x∈x→∃f∀x∈𝒫Xx≠∅→f⁡x∈x
21 13 20 syl ⊢X∈AC_𝒫X→∃f∀x∈𝒫Xx≠∅→f⁡x∈x
22 dfac8a ⊢X∈AC_𝒫X→∃f∀x∈𝒫Xx≠∅→f⁡x∈x→X∈dom⁡card
23 21 22 mpd ⊢X∈AC_𝒫X→X∈dom⁡card
24 pwexg ⊢X∈dom⁡card→𝒫X∈V
25 numacn ⊢𝒫X∈V→X∈dom⁡card→X∈AC_𝒫X
26 24 25 mpcom ⊢X∈dom⁡card→X∈AC_𝒫X
27 23 26 impbii ⊢X∈AC_𝒫X↔X∈dom⁡card