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 )