Definition df-womni 7140

Description: A weakly 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 not. Generalization of definition 2.4 of [Pierik], p. 9.

In particular, om e. 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 = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }

Distinct variable group:   x, f, y

Detailed syntax breakdown of Definition df-womni

Step	Hyp	Ref	Expression
1		cwomni 7139	. 2 class WOmni
2		vy	. . . . . . 7 setvar y
3	2	cv 1347	. . . . . 6 class y
4		c2o 6389	. . . . . 6 class 2o
5		vf	. . . . . . 7 setvar f
6	5	cv 1347	. . . . . 6 class f
7	3, 4, 6	wf 5194	. . . . 5 wff f : y --> 2o
8		vx	. . . . . . . . . 10 setvar x
9	8	cv 1347	. . . . . . . . 9 class x
10	9, 6	cfv 5198	. . . . . . . 8 class ( f ` x )
11		c1o 6388	. . . . . . . 8 class 1o
12	10, 11	wceq 1348	. . . . . . 7 wff ( f ` x ) = 1o
13	12, 8, 3	wral 2448	. . . . . 6 wff A. x e. y ( f ` x ) = 1o
14	13	wdc 829	. . . . 5 wff DECID A. x e. y ( f ` x ) = 1o
15	7, 14	wi 4	. . . 4 wff ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o )
16	15, 5	wal 1346	. . 3 wff A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o )
17	16, 2	cab 2156	. 2 class { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
18	1, 17	wceq 1348	1 wff WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }

This definition is referenced by:  iswomni  7141