Definition df-womni 7140

Description: A weakly omniscient set is one where we can decide whether a predicate (here represented by a function 𝑓) holds (is equal to 1_o) for all elements or not. Generalization of definition 2.4 of [Pierik], p. 9.

In particular, ω ∈ WOmni is known as the Weak Limited Principle of Omniscience (WLPO).

The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)

Assertion

Ref	Expression
df-womni	⊢ WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)}

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-womni

Step	Hyp	Ref	Expression
1		cwomni 7139	. 2 class WOmni
2		vy	. . . . . . 7 setvar 𝑦
3	2	cv 1347	. . . . . 6 class 𝑦
4		c2o 6389	. . . . . 6 class 2o
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1347	. . . . . 6 class 𝑓
7	3, 4, 6	wf 5194	. . . . 5 wff 𝑓:𝑦⟶2o
8		vx	. . . . . . . . . 10 setvar 𝑥
9	8	cv 1347	. . . . . . . . 9 class 𝑥
10	9, 6	cfv 5198	. . . . . . . 8 class (𝑓‘𝑥)
11		c1o 6388	. . . . . . . 8 class 1o
12	10, 11	wceq 1348	. . . . . . 7 wff (𝑓‘𝑥) = 1o
13	12, 8, 3	wral 2448	. . . . . 6 wff ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o
14	13	wdc 829	. . . . 5 wff DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o
15	7, 14	wi 4	. . . 4 wff (𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)
16	15, 5	wal 1346	. . 3 wff ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)
17	16, 2	cab 2156	. 2 class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)}
18	1, 17	wceq 1348	1 wff WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)}

This definition is referenced by:  iswomni  7141