Definition df-markov 7128

Description: A Markov set is one where if a predicate (here represented by a function f) on that set does not hold (where hold means is equal to 1o) for all elements, then there exists an element where it fails (is equal to (/)). Generalization of definition 2.5 of [Pierik], p. 9.

In particular, om e. Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)

Assertion

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

Distinct variable group:   x, f, y

Detailed syntax breakdown of Definition df-markov

Step	Hyp	Ref	Expression
1		cmarkov 7127	. 2 class Markov
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	. . . . . . . . . . 11 setvar x
9	8	cv 1347	. . . . . . . . . 10 class x
10	9, 6	cfv 5198	. . . . . . . . 9 class ( f ` x )
11		c1o 6388	. . . . . . . . 9 class 1o
12	10, 11	wceq 1348	. . . . . . . 8 wff ( f ` x ) = 1o
13	12, 8, 3	wral 2448	. . . . . . 7 wff A. x e. y ( f ` x ) = 1o
14	13	wn 3	. . . . . 6 wff -. A. x e. y ( f ` x ) = 1o
15		c0 3414	. . . . . . . 8 class (/)
16	10, 15	wceq 1348	. . . . . . 7 wff ( f ` x ) = (/)
17	16, 8, 3	wrex 2449	. . . . . 6 wff E. x e. y ( f ` x ) = (/)
18	14, 17	wi 4	. . . . 5 wff ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) )
19	7, 18	wi 4	. . . 4 wff ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) )
20	19, 5	wal 1346	. . 3 wff A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) )
21	20, 2	cab 2156	. 2 class { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
22	1, 21	wceq 1348	1 wff Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }

This definition is referenced by:  ismkv  7129