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

Definition df-omni 7061
 Description: An omniscient set is one where we can decide whether a predicate (here represented by a function ) holds (is equal to ) 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-omni
StepHypRef Expression
1 comni 7060 . 2 Omni
2 vy . . . . . . 7
32cv 1334 . . . . . 6
4 c2o 6351 . . . . . 6
5 vf . . . . . . 7
65cv 1334 . . . . . 6
73, 4, 6wf 5163 . . . . 5
8 vx . . . . . . . . . 10
98cv 1334 . . . . . . . . 9
109, 6cfv 5167 . . . . . . . 8
11 c0 3394 . . . . . . . 8
1210, 11wceq 1335 . . . . . . 7
1312, 8, 3wrex 2436 . . . . . 6
14 c1o 6350 . . . . . . . 8
1510, 14wceq 1335 . . . . . . 7
1615, 8, 3wral 2435 . . . . . 6
1713, 16wo 698 . . . . 5
187, 17wi 4 . . . 4
1918, 5wal 1333 . . 3
2019, 2cab 2143 . 2
211, 20wceq 1335 1 Omni
 Colors of variables: wff set class This definition is referenced by:  isomni  7062
 Copyright terms: Public domain W3C validator