Definition df-omni 7006

Description: An 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 fails to hold (is equal to ∅) for some element. Definition 3.1 of [Pierik], p. 14.

In particular, ω ∈ Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.)

Assertion

Ref	Expression
df-omni	⊢ Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))}

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-omni

Step	Hyp	Ref	Expression
1		comni 7004	. 2 class Omni
2		vy	. . . . . . 7 setvar 𝑦
3	2	cv 1330	. . . . . 6 class 𝑦
4		c2o 6307	. . . . . 6 class 2o
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1330	. . . . . 6 class 𝑓
7	3, 4, 6	wf 5119	. . . . 5 wff 𝑓:𝑦⟶2o
8		vx	. . . . . . . . . 10 setvar 𝑥
9	8	cv 1330	. . . . . . . . 9 class 𝑥
10	9, 6	cfv 5123	. . . . . . . 8 class (𝑓‘𝑥)
11		c0 3363	. . . . . . . 8 class ∅
12	10, 11	wceq 1331	. . . . . . 7 wff (𝑓‘𝑥) = ∅
13	12, 8, 3	wrex 2417	. . . . . 6 wff ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅
14		c1o 6306	. . . . . . . 8 class 1o
15	10, 14	wceq 1331	. . . . . . 7 wff (𝑓‘𝑥) = 1o
16	15, 8, 3	wral 2416	. . . . . 6 wff ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o
17	13, 16	wo 697	. . . . 5 wff (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)
18	7, 17	wi 4	. . . 4 wff (𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))
19	18, 5	wal 1329	. . 3 wff ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))
20	19, 2	cab 2125	. 2 class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))}
21	1, 20	wceq 1331	1 wff Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))}

This definition is referenced by:  isomni  7008