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	⊢ 𝑥 ∈ V
2		omex	⊢ ω ∈ V
3		isacn	⊢ ( ( 𝑥 ∈ V ∧ ω ∈ V ) → ( 𝑥 ∈ AC ω ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) ∃ 𝑔 ∀ 𝑦 ∈ ω ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
4	1 2 3	mp2an	⊢ ( 𝑥 ∈ AC ω ↔ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) ∃ 𝑔 ∀ 𝑦 ∈ ω ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) )
5		axcc2	⊢ ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑦 ∈ ω ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
6		elmapi	⊢ ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) → 𝑓 : ω ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) )
7		ffvelrn	⊢ ( ( 𝑓 : ω ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) ∧ 𝑦 ∈ ω ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝒫 𝑥 ∖ { ∅ } ) )
8		eldifsni	⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ ( 𝒫 𝑥 ∖ { ∅ } ) → ( 𝑓 ‘ 𝑦 ) ≠ ∅ )
9	7 8	syl	⊢ ( ( 𝑓 : ω ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) ∧ 𝑦 ∈ ω ) → ( 𝑓 ‘ 𝑦 ) ≠ ∅ )
10	6 9	sylan	⊢ ( ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) ∧ 𝑦 ∈ ω ) → ( 𝑓 ‘ 𝑦 ) ≠ ∅ )
11		id	⊢ ( ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) → ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
12	10 11	syl5com	⊢ ( ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) ∧ 𝑦 ∈ ω ) → ( ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
13	12	ralimdva	⊢ ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) → ( ∀ 𝑦 ∈ ω ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ω ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
14	13	adantld	⊢ ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) → ( ( 𝑔 Fn ω ∧ ∀ 𝑦 ∈ ω ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ ω ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
15	14	eximdv	⊢ ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) → ( ∃ 𝑔 ( 𝑔 Fn ω ∧ ∀ 𝑦 ∈ ω ( ( 𝑓 ‘ 𝑦 ) ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) ) → ∃ 𝑔 ∀ 𝑦 ∈ ω ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
16	5 15	mpi	⊢ ( 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m ω ) → ∃ 𝑔 ∀ 𝑦 ∈ ω ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) )
17	4 16	mprgbir	⊢ 𝑥 ∈ AC ω
18	17 1	2th	⊢ ( 𝑥 ∈ AC ω ↔ 𝑥 ∈ V )
19	18	eqriv	⊢ AC ω = V