Definition df-vdwpc

Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc for more information. (Contributed by Mario Carneiro, 18-Aug-2014)

	Ref	Expression
Assertion	df-vdwpc	⊢ PolyAP = { ⟨ ⟨ 𝑚 , 𝑘 ⟩ , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvdwp	⊢ PolyAP
1		vm	⊢ 𝑚
2		vk	⊢ 𝑘
3		vf	⊢ 𝑓
4		va	⊢ 𝑎
5		cn	⊢ ℕ
6		vd	⊢ 𝑑
7		cmap	⊢ ↑m
8		c1	⊢ 1
9		cfz	⊢ ...
10	1	cv	⊢ 𝑚
11	8 10 9	co	⊢ ( 1 ... 𝑚 )
12	5 11 7	co	⊢ ( ℕ ↑m ( 1 ... 𝑚 ) )
13		vi	⊢ 𝑖
14	4	cv	⊢ 𝑎
15		caddc	⊢ +
16	6	cv	⊢ 𝑑
17	13	cv	⊢ 𝑖
18	17 16	cfv	⊢ ( 𝑑 ‘ 𝑖 )
19	14 18 15	co	⊢ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) )
20		cvdwa	⊢ AP
21	2	cv	⊢ 𝑘
22	21 20	cfv	⊢ ( AP ‘ 𝑘 )
23	19 18 22	co	⊢ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) )
24	3	cv	⊢ 𝑓
25	24	ccnv	⊢ ◡ 𝑓
26	19 24	cfv	⊢ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) )
27	26	csn	⊢ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) }
28	25 27	cima	⊢ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } )
29	23 28	wss	⊢ ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } )
30	29 13 11	wral	⊢ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } )
31		chash	⊢ ♯
32	13 11 26	cmpt	⊢ ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) )
33	32	crn	⊢ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) )
34	33 31	cfv	⊢ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) )
35	34 10	wceq	⊢ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚
36	30 35	wa	⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 )
37	36 6 12	wrex	⊢ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 )
38	37 4 5	wrex	⊢ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 )
39	38 1 2 3	coprab	⊢ { ⟨ ⟨ 𝑚 , 𝑘 ⟩ , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) }
40	0 39	wceq	⊢ PolyAP = { ⟨ ⟨ 𝑚 , 𝑘 ⟩ , 𝑓 ⟩ ∣ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑚 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝑘 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑚 ) ↦ ( 𝑓 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑚 ) }