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

Definition df-omni 7107
Description: An omniscient set is one where we can decide whether a predicate (here represented by a function 𝑓) holds (is equal to 1o) 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
StepHypRef Expression
1 comni 7106 . 2 class Omni
2 vy . . . . . . 7 setvar 𝑦
32cv 1347 . . . . . 6 class 𝑦
4 c2o 6386 . . . . . 6 class 2o
5 vf . . . . . . 7 setvar 𝑓
65cv 1347 . . . . . 6 class 𝑓
73, 4, 6wf 5192 . . . . 5 wff 𝑓:𝑦⟶2o
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1347 . . . . . . . . 9 class 𝑥
109, 6cfv 5196 . . . . . . . 8 class (𝑓𝑥)
11 c0 3414 . . . . . . . 8 class
1210, 11wceq 1348 . . . . . . 7 wff (𝑓𝑥) = ∅
1312, 8, 3wrex 2449 . . . . . 6 wff 𝑥𝑦 (𝑓𝑥) = ∅
14 c1o 6385 . . . . . . . 8 class 1o
1510, 14wceq 1348 . . . . . . 7 wff (𝑓𝑥) = 1o
1615, 8, 3wral 2448 . . . . . 6 wff 𝑥𝑦 (𝑓𝑥) = 1o
1713, 16wo 703 . . . . 5 wff (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1o)
187, 17wi 4 . . . 4 wff (𝑓:𝑦⟶2o → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1o))
1918, 5wal 1346 . . 3 wff 𝑓(𝑓:𝑦⟶2o → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1o))
2019, 2cab 2156 . 2 class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1o))}
211, 20wceq 1348 1 wff Omni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (∃𝑥𝑦 (𝑓𝑥) = ∅ ∨ ∀𝑥𝑦 (𝑓𝑥) = 1o))}
Colors of variables: wff set class
This definition is referenced by:  isomni  7108
  Copyright terms: Public domain W3C validator