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

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 𝐴 ) ∃ 𝑔 ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝑓 ‘ 𝑦 ) ) }