Definition df-vdwmc 15511

Description: Define the "contains a monochromatic AP" predicate. (Contributed by Mario Carneiro, 18-Aug-2014.)

Assertion

Ref	Expression
df-vdwmc	⊢ MonoAP = {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅}

Distinct variable group:   𝑓,𝑐,𝑘

Detailed syntax breakdown of Definition df-vdwmc

Step	Hyp	Ref	Expression
1		cvdwm 15508	. 2 class MonoAP
2		vk	. . . . . . . . 9 setvar 𝑘
3	2	cv 1474	. . . . . . . 8 class 𝑘
4		cvdwa 15507	. . . . . . . 8 class AP
5	3, 4	cfv 5804	. . . . . . 7 class (AP‘𝑘)
6	5	crn 5039	. . . . . 6 class ran (AP‘𝑘)
7		vf	. . . . . . . . . 10 setvar 𝑓
8	7	cv 1474	. . . . . . . . 9 class 𝑓
9	8	ccnv 5037	. . . . . . . 8 class ◡𝑓
10		vc	. . . . . . . . . 10 setvar 𝑐
11	10	cv 1474	. . . . . . . . 9 class 𝑐
12	11	csn 4125	. . . . . . . 8 class {𝑐}
13	9, 12	cima 5041	. . . . . . 7 class (◡𝑓 “ {𝑐})
14	13	cpw 4108	. . . . . 6 class 𝒫 (◡𝑓 “ {𝑐})
15	6, 14	cin 3539	. . . . 5 class (ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐}))
16		c0 3874	. . . . 5 class ∅
17	15, 16	wne 2780	. . . 4 wff (ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅
18	17, 10	wex 1695	. . 3 wff ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅
19	18, 2, 7	copab 4642	. 2 class {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅}
20	1, 19	wceq 1475	1 wff MonoAP = {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅}

This definition is referenced by:  vdwmc  15520