Metamath Proof Explorer

Theorem dfac13

Description: The axiom of choice holds iff every set has choice sequences as long as itself. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion dfac13 ⊢ CHOICE ↔ ∀ x x ∈ AC _ x

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 acacni ⊢ CHOICE ∧ x ∈ V → AC _ x = V
3 2 elvd ⊢ CHOICE → AC _ x = V
4 1 3 eleqtrrid ⊢ CHOICE → x ∈ AC _ x
5 4 alrimiv ⊢ CHOICE → ∀ x x ∈ AC _ x
6 vpwex ⊢ 𝒫 z ∈ V
7 id ⊢ x = 𝒫 z → x = 𝒫 z
8 acneq ⊢ x = 𝒫 z → AC _ x = AC _ 𝒫 z
9 7 8 eleq12d ⊢ x = 𝒫 z → x ∈ AC _ x ↔ 𝒫 z ∈ AC _ 𝒫 z
10 6 9 spcv ⊢ ∀ x x ∈ AC _ x → 𝒫 z ∈ AC _ 𝒫 z
11 vex ⊢ y ∈ V
12 vex ⊢ z ∈ V
13 12 canth2 ⊢ z ≺ 𝒫 z
14 sdomdom ⊢ z ≺ 𝒫 z → z ≼ 𝒫 z
15 acndom2 ⊢ z ≼ 𝒫 z → 𝒫 z ∈ AC _ 𝒫 z → z ∈ AC _ 𝒫 z
16 13 14 15 mp2b ⊢ 𝒫 z ∈ AC _ 𝒫 z → z ∈ AC _ 𝒫 z
17 acnnum ⊢ z ∈ AC _ 𝒫 z ↔ z ∈ dom ⁡ card
18 16 17 sylib ⊢ 𝒫 z ∈ AC _ 𝒫 z → z ∈ dom ⁡ card
19 numacn ⊢ y ∈ V → z ∈ dom ⁡ card → z ∈ AC _ y
20 11 18 19 mpsyl ⊢ 𝒫 z ∈ AC _ 𝒫 z → z ∈ AC _ y
21 10 20 syl ⊢ ∀ x x ∈ AC _ x → z ∈ AC _ y
22 12 a1i ⊢ ∀ x x ∈ AC _ x → z ∈ V
23 21 22 2thd ⊢ ∀ x x ∈ AC _ x → z ∈ AC _ y ↔ z ∈ V
24 23 eqrdv ⊢ ∀ x x ∈ AC _ x → AC _ y = V
25 24 alrimiv ⊢ ∀ x x ∈ AC _ x → ∀ y AC _ y = V
26 dfacacn ⊢ CHOICE ↔ ∀ y AC _ y = V
27 25 26 sylibr ⊢ ∀ x x ∈ AC _ x → CHOICE
28 5 27 impbii ⊢ CHOICE ↔ ∀ x x ∈ AC _ x