This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem finacn

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

Ref Expression
Assertion finacn ( 𝐴 ∈ Fin → AC 𝐴 = V )

Proof

Step Hyp Ref Expression
1 elmapi ⊢ ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) → 𝑓 : 𝐴 ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) )
2 1 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ) → 𝑓 : 𝐴 ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) )
3 ffvelcdm ⊢ ( ( 𝑓 : 𝐴 ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝒫 𝑥 ∖ { ∅ } ) )
4 eldifsni ⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ( 𝒫 𝑥 ∖ { ∅ } ) → ( 𝑓 ‘ 𝑦 ) ≠ ∅ )
5 3 4 syl ⊢ ( ( 𝑓 : 𝐴 ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) ≠ ∅ )
6 n0 ⊢ ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) )
7 5 6 sylib ⊢ ( ( 𝑓 : 𝐴 ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) )
8 rexv ⊢ ( ∃ 𝑧 ∈ V 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑧 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) )
9 7 8 sylibr ⊢ ( ( 𝑓 : 𝐴 ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑧 ∈ V 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) )
10 9 ralrimiva ⊢ ( 𝑓 : 𝐴 ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) → ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ V 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) )
11 2 10 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ V 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) )
12 eleq1 ⊢ ( 𝑧 = ( 𝑔 ‘ 𝑦 ) → ( 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
13 12 ac6sfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ V 𝑧 ∈ ( 𝑓 ‘ 𝑦 ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ V ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
14 11 13 syldan ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ V ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
15 exsimpr ⊢ ( ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ V ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) → ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) )
16 14 15 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ) → ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) )
17 16 ralrimiva ⊢ ( 𝐴 ∈ Fin → ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) )
18 vex ⊢ 𝑥 ∈ V
19 isacn ⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ Fin ) → ( 𝑥 ∈ AC 𝐴 ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
20 18 19 mpan ⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ AC 𝐴 ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
21 17 20 mpbird ⊢ ( 𝐴 ∈ Fin → 𝑥 ∈ AC 𝐴 )
22 18 a1i ⊢ ( 𝐴 ∈ Fin → 𝑥 ∈ V )
23 21 22 2thd ⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ AC 𝐴 ↔ 𝑥 ∈ V ) )
24 23 eqrdv ⊢ ( 𝐴 ∈ Fin → AC 𝐴 = V )