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 15654
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 15651 . 2 class MonoAP
2 vk . . . . . . . . 9 setvar 𝑘
32cv 1480 . . . . . . . 8 class 𝑘
4 cvdwa 15650 . . . . . . . 8 class AP
53, 4cfv 5876 . . . . . . 7 class (AP‘𝑘)
65crn 5105 . . . . . 6 class ran (AP‘𝑘)
7 vf . . . . . . . . . 10 setvar 𝑓
87cv 1480 . . . . . . . . 9 class 𝑓
98ccnv 5103 . . . . . . . 8 class 𝑓
10 vc . . . . . . . . . 10 setvar 𝑐
1110cv 1480 . . . . . . . . 9 class 𝑐
1211csn 4168 . . . . . . . 8 class {𝑐}
139, 12cima 5107 . . . . . . 7 class (𝑓 “ {𝑐})
1413cpw 4149 . . . . . 6 class 𝒫 (𝑓 “ {𝑐})
156, 14cin 3566 . . . . 5 class (ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐}))
16 c0 3907 . . . . 5 class
1715, 16wne 2791 . . . 4 wff (ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅
1817, 10wex 1702 . . 3 wff 𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅
1918, 2, 7copab 4703 . 2 class {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅}
201, 19wceq 1481 1 wff MonoAP = {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅}
Colors of variables: wff setvar class
This definition is referenced by:  vdwmc  15663
  Copyright terms: Public domain W3C validator