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 16666
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 16663 . 2 class MonoAP
2 vk . . . . . . . . 9 setvar 𝑘
32cv 1541 . . . . . . . 8 class 𝑘
4 cvdwa 16662 . . . . . . . 8 class AP
53, 4cfv 6431 . . . . . . 7 class (AP‘𝑘)
65crn 5590 . . . . . 6 class ran (AP‘𝑘)
7 vf . . . . . . . . . 10 setvar 𝑓
87cv 1541 . . . . . . . . 9 class 𝑓
98ccnv 5588 . . . . . . . 8 class 𝑓
10 vc . . . . . . . . . 10 setvar 𝑐
1110cv 1541 . . . . . . . . 9 class 𝑐
1211csn 4567 . . . . . . . 8 class {𝑐}
139, 12cima 5592 . . . . . . 7 class (𝑓 “ {𝑐})
1413cpw 4539 . . . . . 6 class 𝒫 (𝑓 “ {𝑐})
156, 14cin 3891 . . . . 5 class (ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐}))
16 c0 4262 . . . . 5 class
1715, 16wne 2945 . . . 4 wff (ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅
1817, 10wex 1786 . . 3 wff 𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅
1918, 2, 7copab 5141 . 2 class {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅}
201, 19wceq 1542 1 wff MonoAP = {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (𝑓 “ {𝑐})) ≠ ∅}
Colors of variables: wff setvar class
This definition is referenced by:  vdwmc  16675
  Copyright terms: Public domain W3C validator