Metamath Proof Explorer


Definition df-acn

Description: Define a local and length-limited version of the axiom of choice. The definition of the predicate X e. AC_ A is that for all families of nonempty subsets of X indexed on A (i.e. functions A --> ~P X \ { (/) } ), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion df-acn AC 𝐴 = { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 0 wacn AC 𝐴
2 vx 𝑥
3 cvv V
4 0 3 wcel 𝐴 ∈ V
5 vf 𝑓
6 2 cv 𝑥
7 6 cpw 𝒫 𝑥
8 c0
9 8 csn { ∅ }
10 7 9 cdif ( 𝒫 𝑥 ∖ { ∅ } )
11 cmap m
12 10 0 11 co ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 )
13 vg 𝑔
14 vy 𝑦
15 13 cv 𝑔
16 14 cv 𝑦
17 16 15 cfv ( 𝑔𝑦 )
18 5 cv 𝑓
19 16 18 cfv ( 𝑓𝑦 )
20 17 19 wcel ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 )
21 20 14 0 wral 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 )
22 21 13 wex 𝑔𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 )
23 22 5 12 wral 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 )
24 4 23 wa ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) )
25 24 2 cab { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ) }
26 1 25 wceq AC 𝐴 = { 𝑥 ∣ ( 𝐴 ∈ V ∧ ∀ 𝑓 ∈ ( ( 𝒫 𝑥 ∖ { ∅ } ) ↑m 𝐴 ) ∃ 𝑔𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝑓𝑦 ) ) }