Definition df-omni 7133

Description: An omniscient set is one where we can decide whether a predicate (here represented by a function f) 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, om e. Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.)

Assertion

Ref	Expression
df-omni	|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }

Distinct variable group:   x, f, y

Detailed syntax breakdown of Definition df-omni

Step	Hyp	Ref	Expression
1		comni 7132	. 2 class Omni
2		vy	. . . . . . 7 setvar y
3	2	cv 1352	. . . . . 6 class y
4		c2o 6411	. . . . . 6 class 2o
5		vf	. . . . . . 7 setvar f
6	5	cv 1352	. . . . . 6 class f
7	3, 4, 6	wf 5213	. . . . 5 wff f : y --> 2o
8		vx	. . . . . . . . . 10 setvar x
9	8	cv 1352	. . . . . . . . 9 class x
10	9, 6	cfv 5217	. . . . . . . 8 class ( f ` x )
11		c0 3423	. . . . . . . 8 class (/)
12	10, 11	wceq 1353	. . . . . . 7 wff ( f ` x ) = (/)
13	12, 8, 3	wrex 2456	. . . . . 6 wff E. x e. y ( f ` x ) = (/)
14		c1o 6410	. . . . . . . 8 class 1o
15	10, 14	wceq 1353	. . . . . . 7 wff ( f ` x ) = 1o
16	15, 8, 3	wral 2455	. . . . . 6 wff A. x e. y ( f ` x ) = 1o
17	13, 16	wo 708	. . . . 5 wff ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o )
18	7, 17	wi 4	. . . 4 wff ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) )
19	18, 5	wal 1351	. . 3 wff A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) )
20	19, 2	cab 2163	. 2 class { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
21	1, 20	wceq 1353	1 wff Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }

This definition is referenced by:  isomni  7134