MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdwmc Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 cvdwm 15508 . 2 class MonoAP
2 vk . . . . . . . . 9 setvar 𝑘
32cv 1474 . . . . . . . 8 class 𝑘
4 cvdwa 15507 . . . . . . . 8 class AP
53, 4cfv 5804 . . . . . . 7 class (AP‘𝑘)
65crn 5039 . . . . . 6 class ran (AP‘𝑘)
7 vf . . . . . . . . . 10 setvar 𝑓
87cv 1474 . . . . . . . . 9 class 𝑓
98ccnv 5037 . . . . . . . 8 class 𝑓
10 vc . . . . . . . . . 10 setvar 𝑐
1110cv 1474 . . . . . . . . 9 class 𝑐
1211csn 4125 . . . . . . . 8 class {𝑐}
139, 12cima 5041 . . . . . . 7 class (𝑓 “ {𝑐})
1413cpw 4108 . . . . . 6 class 𝒫 (𝑓 “ {𝑐})
156, 14cin 3539 . . . . 5 class (ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐}))
16 c0 3874 . . . . 5 class
1715, 16wne 2780 . . . 4 wff (ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅
1817, 10wex 1695 . . 3 wff 𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅
1918, 2, 7copab 4642 . 2 class {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅}
201, 19wceq 1475 1 wff MonoAP = {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅}
Colors of variables: wff setvar class
This definition is referenced by:  vdwmc  15520
  Copyright terms: Public domain W3C validator