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 x V
2 omex ω V
3 isacn x V ω V x AC _ ω f 𝒫 x ω g y ω g y f y
4 1 2 3 mp2an x AC _ ω f 𝒫 x ω g y ω g y f y
5 axcc2 g g Fn ω y ω f y g y f y
6 elmapi f 𝒫 x ω f : ω 𝒫 x
7 ffvelrn f : ω 𝒫 x y ω f y 𝒫 x
8 eldifsni f y 𝒫 x f y
9 7 8 syl f : ω 𝒫 x y ω f y
10 6 9 sylan f 𝒫 x ω y ω f y
11 id f y g y f y f y g y f y
12 10 11 syl5com f 𝒫 x ω y ω f y g y f y g y f y
13 12 ralimdva f 𝒫 x ω y ω f y g y f y y ω g y f y
14 13 adantld f 𝒫 x ω g Fn ω y ω f y g y f y y ω g y f y
15 14 eximdv f 𝒫 x ω g g Fn ω y ω f y g y f y g y ω g y f y
16 5 15 mpi f 𝒫 x ω g y ω g y f y
17 4 16 mprgbir x AC _ ω
18 17 1 2th x AC _ ω x V
19 18 eqriv AC _ ω = V