Metamath Proof Explorer

Theorem acncc

Description: An ax-cc equivalent: every set has choice sets of length _om . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acncc ⊢ AC _ ω = V

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 omex ⊢ ω ∈ V
3 isacn ⊢ x ∈ V ∧ ω ∈ V → x ∈ AC _ ω ↔ ∀ f ∈ 𝒫 x ∖ ∅ ω ∃ g ∀ y ∈ ω g ⁡ y ∈ f ⁡ y
4 1 2 3 mp2an ⊢ x ∈ AC _ ω ↔ ∀ f ∈ 𝒫 x ∖ ∅ ω ∃ g ∀ y ∈ ω g ⁡ y ∈ f ⁡ y
5 axcc2 ⊢ ∃ g g Fn ω ∧ ∀ y ∈ ω f ⁡ y ≠ ∅ → g ⁡ y ∈ f ⁡ y
6 elmapi ⊢ f ∈ 𝒫 x ∖ ∅ ω → f : ω ⟶ 𝒫 x ∖ ∅
7 ffvelrn ⊢ f : ω ⟶ 𝒫 x ∖ ∅ ∧ y ∈ ω → f ⁡ y ∈ 𝒫 x ∖ ∅
8 eldifsni ⊢ f ⁡ y ∈ 𝒫 x ∖ ∅ → f ⁡ y ≠ ∅
9 7 8 syl ⊢ f : ω ⟶ 𝒫 x ∖ ∅ ∧ y ∈ ω → f ⁡ y ≠ ∅
10 6 9 sylan ⊢ f ∈ 𝒫 x ∖ ∅ ω ∧ y ∈ ω → f ⁡ y ≠ ∅
11 id ⊢ f ⁡ y ≠ ∅ → g ⁡ y ∈ f ⁡ y → f ⁡ y ≠ ∅ → g ⁡ y ∈ f ⁡ y
12 10 11 syl5com ⊢ f ∈ 𝒫 x ∖ ∅ ω ∧ y ∈ ω → f ⁡ y ≠ ∅ → g ⁡ y ∈ f ⁡ y → g ⁡ y ∈ f ⁡ y
13 12 ralimdva ⊢ f ∈ 𝒫 x ∖ ∅ ω → ∀ y ∈ ω f ⁡ y ≠ ∅ → g ⁡ y ∈ f ⁡ y → ∀ y ∈ ω g ⁡ y ∈ f ⁡ y
14 13 adantld ⊢ f ∈ 𝒫 x ∖ ∅ ω → g Fn ω ∧ ∀ y ∈ ω f ⁡ y ≠ ∅ → g ⁡ y ∈ f ⁡ y → ∀ y ∈ ω g ⁡ y ∈ f ⁡ y
15 14 eximdv ⊢ f ∈ 𝒫 x ∖ ∅ ω → ∃ g g Fn ω ∧ ∀ y ∈ ω f ⁡ y ≠ ∅ → g ⁡ y ∈ f ⁡ y → ∃ g ∀ y ∈ ω g ⁡ y ∈ f ⁡ y
16 5 15 mpi ⊢ f ∈ 𝒫 x ∖ ∅ ω → ∃ g ∀ y ∈ ω g ⁡ y ∈ f ⁡ y
17 4 16 mprgbir ⊢ x ∈ AC _ ω
18 17 1 2th ⊢ x ∈ AC _ ω ↔ x ∈ V
19 18 eqriv ⊢ AC _ ω = V