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

Definition df-acn 9937
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 ∧ βˆ€π‘“ ∈ ((𝒫 π‘₯ βˆ– {βˆ…}) ↑m 𝐴)βˆƒπ‘”βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦))}
Distinct variable group:   𝑓,𝑔,π‘₯,𝑦,𝐴

Detailed syntax breakdown of Definition df-acn
StepHypRef Expression
1 cA . . 3 class 𝐴
21wacn 9933 . 2 class AC 𝐴
3 cvv 3475 . . . . 5 class V
41, 3wcel 2107 . . . 4 wff 𝐴 ∈ V
5 vy . . . . . . . . . 10 setvar 𝑦
65cv 1541 . . . . . . . . 9 class 𝑦
7 vg . . . . . . . . . 10 setvar 𝑔
87cv 1541 . . . . . . . . 9 class 𝑔
96, 8cfv 6544 . . . . . . . 8 class (π‘”β€˜π‘¦)
10 vf . . . . . . . . . 10 setvar 𝑓
1110cv 1541 . . . . . . . . 9 class 𝑓
126, 11cfv 6544 . . . . . . . 8 class (π‘“β€˜π‘¦)
139, 12wcel 2107 . . . . . . 7 wff (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦)
1413, 5, 1wral 3062 . . . . . 6 wff βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦)
1514, 7wex 1782 . . . . 5 wff βˆƒπ‘”βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦)
16 vx . . . . . . . . 9 setvar π‘₯
1716cv 1541 . . . . . . . 8 class π‘₯
1817cpw 4603 . . . . . . 7 class 𝒫 π‘₯
19 c0 4323 . . . . . . . 8 class βˆ…
2019csn 4629 . . . . . . 7 class {βˆ…}
2118, 20cdif 3946 . . . . . 6 class (𝒫 π‘₯ βˆ– {βˆ…})
22 cmap 8820 . . . . . 6 class ↑m
2321, 1, 22co 7409 . . . . 5 class ((𝒫 π‘₯ βˆ– {βˆ…}) ↑m 𝐴)
2415, 10, 23wral 3062 . . . 4 wff βˆ€π‘“ ∈ ((𝒫 π‘₯ βˆ– {βˆ…}) ↑m 𝐴)βˆƒπ‘”βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦)
254, 24wa 397 . . 3 wff (𝐴 ∈ V ∧ βˆ€π‘“ ∈ ((𝒫 π‘₯ βˆ– {βˆ…}) ↑m 𝐴)βˆƒπ‘”βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦))
2625, 16cab 2710 . 2 class {π‘₯ ∣ (𝐴 ∈ V ∧ βˆ€π‘“ ∈ ((𝒫 π‘₯ βˆ– {βˆ…}) ↑m 𝐴)βˆƒπ‘”βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦))}
272, 26wceq 1542 1 wff AC 𝐴 = {π‘₯ ∣ (𝐴 ∈ V ∧ βˆ€π‘“ ∈ ((𝒫 π‘₯ βˆ– {βˆ…}) ↑m 𝐴)βˆƒπ‘”βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ (π‘“β€˜π‘¦))}
Colors of variables: wff setvar class
This definition is referenced by:  acnrcl  10037  acneq  10038  isacn  10039
  Copyright terms: Public domain W3C validator