ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-cc GIF version

Definition df-cc 7091
Description: The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7075 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
Assertion
Ref Expression
df-cc (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓𝑥𝑓 Fn dom 𝑥)))
Distinct variable group:   𝑥,𝑓

Detailed syntax breakdown of Definition df-cc
StepHypRef Expression
1 wacc 7090 . 2 wff CCHOICE
2 vx . . . . . . 7 setvar 𝑥
32cv 1331 . . . . . 6 class 𝑥
43cdm 4543 . . . . 5 class dom 𝑥
5 com 4508 . . . . 5 class ω
6 cen 6636 . . . . 5 class
74, 5, 6wbr 3933 . . . 4 wff dom 𝑥 ≈ ω
8 vf . . . . . . . 8 setvar 𝑓
98cv 1331 . . . . . . 7 class 𝑓
109, 3wss 3072 . . . . . 6 wff 𝑓𝑥
119, 4wfn 5122 . . . . . 6 wff 𝑓 Fn dom 𝑥
1210, 11wa 103 . . . . 5 wff (𝑓𝑥𝑓 Fn dom 𝑥)
1312, 8wex 1469 . . . 4 wff 𝑓(𝑓𝑥𝑓 Fn dom 𝑥)
147, 13wi 4 . . 3 wff (dom 𝑥 ≈ ω → ∃𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
1514, 2wal 1330 . 2 wff 𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓𝑥𝑓 Fn dom 𝑥))
161, 15wb 104 1 wff (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓𝑥𝑓 Fn dom 𝑥)))
Colors of variables: wff set class
This definition is referenced by:  ccfunen  7092
  Copyright terms: Public domain W3C validator