Metamath Proof Explorer

Theorem finacn

Description: Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion finacn ⊢ A ∈ Fin → AC _ A = V

Proof

Step Hyp Ref Expression
1 elmapi ⊢ f ∈ 𝒫 x ∖ ∅ A → f : A ⟶ 𝒫 x ∖ ∅
2 1 adantl ⊢ A ∈ Fin ∧ f ∈ 𝒫 x ∖ ∅ A → f : A ⟶ 𝒫 x ∖ ∅
3 ffvelrn ⊢ f : A ⟶ 𝒫 x ∖ ∅ ∧ y ∈ A → f ⁡ y ∈ 𝒫 x ∖ ∅
4 eldifsni ⊢ f ⁡ y ∈ 𝒫 x ∖ ∅ → f ⁡ y ≠ ∅
5 3 4 syl ⊢ f : A ⟶ 𝒫 x ∖ ∅ ∧ y ∈ A → f ⁡ y ≠ ∅
6 n0 ⊢ f ⁡ y ≠ ∅ ↔ ∃ z z ∈ f ⁡ y
7 5 6 sylib ⊢ f : A ⟶ 𝒫 x ∖ ∅ ∧ y ∈ A → ∃ z z ∈ f ⁡ y
8 rexv ⊢ ∃ z ∈ V z ∈ f ⁡ y ↔ ∃ z z ∈ f ⁡ y
9 7 8 sylibr ⊢ f : A ⟶ 𝒫 x ∖ ∅ ∧ y ∈ A → ∃ z ∈ V z ∈ f ⁡ y
10 9 ralrimiva ⊢ f : A ⟶ 𝒫 x ∖ ∅ → ∀ y ∈ A ∃ z ∈ V z ∈ f ⁡ y
11 2 10 syl ⊢ A ∈ Fin ∧ f ∈ 𝒫 x ∖ ∅ A → ∀ y ∈ A ∃ z ∈ V z ∈ f ⁡ y
12 eleq1 ⊢ z = g ⁡ y → z ∈ f ⁡ y ↔ g ⁡ y ∈ f ⁡ y
13 12 ac6sfi ⊢ A ∈ Fin ∧ ∀ y ∈ A ∃ z ∈ V z ∈ f ⁡ y → ∃ g g : A ⟶ V ∧ ∀ y ∈ A g ⁡ y ∈ f ⁡ y
14 11 13 syldan ⊢ A ∈ Fin ∧ f ∈ 𝒫 x ∖ ∅ A → ∃ g g : A ⟶ V ∧ ∀ y ∈ A g ⁡ y ∈ f ⁡ y
15 exsimpr ⊢ ∃ g g : A ⟶ V ∧ ∀ y ∈ A g ⁡ y ∈ f ⁡ y → ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
16 14 15 syl ⊢ A ∈ Fin ∧ f ∈ 𝒫 x ∖ ∅ A → ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
17 16 ralrimiva ⊢ A ∈ Fin → ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
18 vex ⊢ x ∈ V
19 isacn ⊢ x ∈ V ∧ A ∈ Fin → x ∈ AC _ A ↔ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
20 18 19 mpan ⊢ A ∈ Fin → x ∈ AC _ A ↔ ∀ f ∈ 𝒫 x ∖ ∅ A ∃ g ∀ y ∈ A g ⁡ y ∈ f ⁡ y
21 17 20 mpbird ⊢ A ∈ Fin → x ∈ AC _ A
22 18 a1i ⊢ A ∈ Fin → x ∈ V
23 21 22 2thd ⊢ A ∈ Fin → x ∈ AC _ A ↔ x ∈ V
24 23 eqrdv ⊢ A ∈ Fin → AC _ A = V