Definition df-cc 7257

Description: The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7200 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

Step	Hyp	Ref	Expression
1		wacc 7256	. 2 wff CCHOICE
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1352	. . . . . 6 class 𝑥
4	3	cdm 4624	. . . . 5 class dom 𝑥
5		com 4587	. . . . 5 class ω
6		cen 6733	. . . . 5 class ≈
7	4, 5, 6	wbr 4001	. . . 4 wff dom 𝑥 ≈ ω
8		vf	. . . . . . . 8 setvar 𝑓
9	8	cv 1352	. . . . . . 7 class 𝑓
10	9, 3	wss 3129	. . . . . 6 wff 𝑓 ⊆ 𝑥
11	9, 4	wfn 5208	. . . . . 6 wff 𝑓 Fn dom 𝑥
12	10, 11	wa 104	. . . . 5 wff (𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)
13	12, 8	wex 1492	. . . 4 wff ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)
14	7, 13	wi 4	. . 3 wff (dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))
15	14, 2	wal 1351	. 2 wff ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))
16	1, 15	wb 105	1 wff (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)))

This definition is referenced by:  ccfunen  7258