Definition df-markov 7128

Description: A Markov set is one where if a predicate (here represented by a function 𝑓) on that set does not hold (where hold means is equal to 1_o) 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, ω ∈ Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)

Assertion

Ref	Expression
df-markov	⊢ Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))}

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-markov

Step	Hyp	Ref	Expression
1		cmarkov 7127	. 2 class Markov
2		vy	. . . . . . 7 setvar 𝑦
3	2	cv 1347	. . . . . 6 class 𝑦
4		c2o 6389	. . . . . 6 class 2o
5		vf	. . . . . . 7 setvar 𝑓
6	5	cv 1347	. . . . . 6 class 𝑓
7	3, 4, 6	wf 5194	. . . . 5 wff 𝑓:𝑦⟶2o
8		vx	. . . . . . . . . . 11 setvar 𝑥
9	8	cv 1347	. . . . . . . . . 10 class 𝑥
10	9, 6	cfv 5198	. . . . . . . . 9 class (𝑓‘𝑥)
11		c1o 6388	. . . . . . . . 9 class 1o
12	10, 11	wceq 1348	. . . . . . . 8 wff (𝑓‘𝑥) = 1o
13	12, 8, 3	wral 2448	. . . . . . 7 wff ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o
14	13	wn 3	. . . . . 6 wff ¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o
15		c0 3414	. . . . . . . 8 class ∅
16	10, 15	wceq 1348	. . . . . . 7 wff (𝑓‘𝑥) = ∅
17	16, 8, 3	wrex 2449	. . . . . 6 wff ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅
18	14, 17	wi 4	. . . . 5 wff (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅)
19	7, 18	wi 4	. . . 4 wff (𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))
20	19, 5	wal 1346	. . 3 wff ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))
21	20, 2	cab 2156	. 2 class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))}
22	1, 21	wceq 1348	1 wff Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅))}

This definition is referenced by:  ismkv  7129