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 ffvelcdm ⊢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≠∅↔∃zz∈f⁡y
7 5 6 sylib ⊢f:A⟶𝒫x∖∅∧y∈A→∃zz∈f⁡y
8 rexv ⊢∃z∈Vz∈f⁡y↔∃zz∈f⁡y
9 7 8 sylibr ⊢f:A⟶𝒫x∖∅∧y∈A→∃z∈Vz∈f⁡y
10 9 ralrimiva ⊢f:A⟶𝒫x∖∅→∀y∈A∃z∈Vz∈f⁡y
11 2 10 syl ⊢A∈Fin∧f∈𝒫x∖∅A→∀y∈A∃z∈Vz∈f⁡y
12 eleq1 ⊢z=g⁡y→z∈f⁡y↔g⁡y∈f⁡y
13 12 ac6sfi ⊢A∈Fin∧∀y∈A∃z∈Vz∈f⁡y→∃gg:A⟶V∧∀y∈Ag⁡y∈f⁡y
14 11 13 syldan ⊢A∈Fin∧f∈𝒫x∖∅A→∃gg:A⟶V∧∀y∈Ag⁡y∈f⁡y
15 exsimpr ⊢∃gg:A⟶V∧∀y∈Ag⁡y∈f⁡y→∃g∀y∈Ag⁡y∈f⁡y
16 14 15 syl ⊢A∈Fin∧f∈𝒫x∖∅A→∃g∀y∈Ag⁡y∈f⁡y
17 16 ralrimiva ⊢A∈Fin→∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y
18 vex ⊢x∈V
19 isacn ⊢x∈V∧A∈Fin→x∈AC_A↔∀f∈𝒫x∖∅A∃g∀y∈Ag⁡y∈f⁡y
20 18 19 mpan ⊢A∈Fin→x∈AC_A↔∀f∈𝒫x∖∅A∃g∀y∈Ag⁡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