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

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝑓 : ω ⟶ ( 𝒫 𝑥 ∖ { ∅ } ) ∧ 𝑦 ∈ ω ) → ( 𝑓 ‘ 𝑦 ) ∈ ( 𝒫 𝑥 ∖ { ∅ } ) )
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