Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-acn Structured version   Visualization version   GIF version

Definition df-acn 8651
 Description: Define a local and length-limited version of the axiom of choice. The definition of the predicate 𝑋 ∈ AC 𝐴 is that for all families of nonempty subsets of 𝑋 indexed on 𝐴 (i.e. functions 𝐴⟶𝒫 𝑋 ∖ {∅}), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
df-acn AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔𝑦𝐴 (𝑔𝑦) ∈ (𝑓𝑦))}
Distinct variable group:   𝑓,𝑔,𝑥,𝑦,𝐴

Detailed syntax breakdown of Definition df-acn
StepHypRef Expression
1 cA . . 3 class 𝐴
21wacn 8647 . 2 class AC 𝐴
3 cvv 3173 . . . . 5 class V
41, 3wcel 1977 . . . 4 wff 𝐴 ∈ V
5 vy . . . . . . . . . 10 setvar 𝑦
65cv 1474 . . . . . . . . 9 class 𝑦
7 vg . . . . . . . . . 10 setvar 𝑔
87cv 1474 . . . . . . . . 9 class 𝑔
96, 8cfv 5804 . . . . . . . 8 class (𝑔𝑦)
10 vf . . . . . . . . . 10 setvar 𝑓
1110cv 1474 . . . . . . . . 9 class 𝑓
126, 11cfv 5804 . . . . . . . 8 class (𝑓𝑦)
139, 12wcel 1977 . . . . . . 7 wff (𝑔𝑦) ∈ (𝑓𝑦)
1413, 5, 1wral 2896 . . . . . 6 wff 𝑦𝐴 (𝑔𝑦) ∈ (𝑓𝑦)
1514, 7wex 1695 . . . . 5 wff 𝑔𝑦𝐴 (𝑔𝑦) ∈ (𝑓𝑦)
16 vx . . . . . . . . 9 setvar 𝑥
1716cv 1474 . . . . . . . 8 class 𝑥
1817cpw 4108 . . . . . . 7 class 𝒫 𝑥
19 c0 3874 . . . . . . . 8 class
2019csn 4125 . . . . . . 7 class {∅}
2118, 20cdif 3537 . . . . . 6 class (𝒫 𝑥 ∖ {∅})
22 cmap 7744 . . . . . 6 class 𝑚
2321, 1, 22co 6549 . . . . 5 class ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)
2415, 10, 23wral 2896 . . . 4 wff 𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔𝑦𝐴 (𝑔𝑦) ∈ (𝑓𝑦)
254, 24wa 383 . . 3 wff (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔𝑦𝐴 (𝑔𝑦) ∈ (𝑓𝑦))
2625, 16cab 2596 . 2 class {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔𝑦𝐴 (𝑔𝑦) ∈ (𝑓𝑦))}
272, 26wceq 1475 1 wff AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔𝑦𝐴 (𝑔𝑦) ∈ (𝑓𝑦))}
 Colors of variables: wff setvar class This definition is referenced by:  acnrcl  8748  acneq  8749  isacn  8750
 Copyright terms: Public domain W3C validator