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 ( 𝑋 ∈ AC 𝒫 𝑋 ↔ 𝑋 ∈ dom card )

Proof

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