Definition df-vdwmc

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvdwm	⊢ MonoAP
1		vk	⊢ 𝑘
2		vf	⊢ 𝑓
3		vc	⊢ 𝑐
4		cvdwa	⊢ AP
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( AP ‘ 𝑘 )
7	6	crn	⊢ ran ( AP ‘ 𝑘 )
8	2	cv	⊢ 𝑓
9	8	ccnv	⊢ ◡ 𝑓
10	3	cv	⊢ 𝑐
11	10	csn	⊢ { 𝑐 }
12	9 11	cima	⊢ ( ◡ 𝑓 “ { 𝑐 } )
13	12	cpw	⊢ 𝒫 ( ◡ 𝑓 “ { 𝑐 } )
14	7 13	cin	⊢ ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) )
15		c0	⊢ ∅
16	14 15	wne	⊢ ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) ≠ ∅
17	16 3	wex	⊢ ∃ 𝑐 ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) ≠ ∅
18	17 1 2	copab	⊢ { ⟨ 𝑘 , 𝑓 ⟩ ∣ ∃ 𝑐 ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) ≠ ∅ }
19	0 18	wceq	⊢ MonoAP = { ⟨ 𝑘 , 𝑓 ⟩ ∣ ∃ 𝑐 ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) ≠ ∅ }