Metamath Proof Explorer

Theorem vdwmc

Description: The predicate " The <. R , N >. -coloring F contains a monochromatic AP of length K ". (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwmc.1 ⊢ X ∈ V
vdwmc.2 ⊢ φ → K ∈ ℕ 0
vdwmc.3 ⊢ φ → F : X ⟶ R
Assertion vdwmc ⊢ φ → K MonoAP F ↔ ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c

Proof

Step Hyp Ref Expression
1 vdwmc.1 ⊢ X ∈ V
2 vdwmc.2 ⊢ φ → K ∈ ℕ 0
3 vdwmc.3 ⊢ φ → F : X ⟶ R
4 fex ⊢ F : X ⟶ R ∧ X ∈ V → F ∈ V
5 3 1 4 sylancl ⊢ φ → F ∈ V
6 fveq2 ⊢ k = K → AP ⁡ k = AP ⁡ K
7 6 rneqd ⊢ k = K → ran ⁡ AP ⁡ k = ran ⁡ AP ⁡ K
8 cnveq ⊢ f = F → f -1 = F -1
9 8 imaeq1d ⊢ f = F → f -1 c = F -1 c
10 9 pweqd ⊢ f = F → 𝒫 f -1 c = 𝒫 F -1 c
11 7 10 ineqan12d ⊢ k = K ∧ f = F → ran ⁡ AP ⁡ k ∩ 𝒫 f -1 c = ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c
12 11 neeq1d ⊢ k = K ∧ f = F → ran ⁡ AP ⁡ k ∩ 𝒫 f -1 c ≠ ∅ ↔ ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅
13 12 exbidv ⊢ k = K ∧ f = F → ∃ c ran ⁡ AP ⁡ k ∩ 𝒫 f -1 c ≠ ∅ ↔ ∃ c ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅
14 df-vdwmc ⊢ MonoAP = k f | ∃ c ran ⁡ AP ⁡ k ∩ 𝒫 f -1 c ≠ ∅
15 13 14 brabga ⊢ K ∈ ℕ 0 ∧ F ∈ V → K MonoAP F ↔ ∃ c ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅
16 2 5 15 syl2anc ⊢ φ → K MonoAP F ↔ ∃ c ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅
17 vdwapf ⊢ K ∈ ℕ 0 → AP ⁡ K : ℕ × ℕ ⟶ 𝒫 ℕ
18 ffn ⊢ AP ⁡ K : ℕ × ℕ ⟶ 𝒫 ℕ → AP ⁡ K Fn ℕ × ℕ
19 velpw ⊢ z ∈ 𝒫 F -1 c ↔ z ⊆ F -1 c
20 sseq1 ⊢ z = AP ⁡ K ⁡ w → z ⊆ F -1 c ↔ AP ⁡ K ⁡ w ⊆ F -1 c
21 19 20 syl5bb ⊢ z = AP ⁡ K ⁡ w → z ∈ 𝒫 F -1 c ↔ AP ⁡ K ⁡ w ⊆ F -1 c
22 21 rexrn ⊢ AP ⁡ K Fn ℕ × ℕ → ∃ z ∈ ran ⁡ AP ⁡ K z ∈ 𝒫 F -1 c ↔ ∃ w ∈ ℕ × ℕ AP ⁡ K ⁡ w ⊆ F -1 c
23 2 17 18 22 4syl ⊢ φ → ∃ z ∈ ran ⁡ AP ⁡ K z ∈ 𝒫 F -1 c ↔ ∃ w ∈ ℕ × ℕ AP ⁡ K ⁡ w ⊆ F -1 c
24 elin ⊢ z ∈ ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ↔ z ∈ ran ⁡ AP ⁡ K ∧ z ∈ 𝒫 F -1 c
25 24 exbii ⊢ ∃ z z ∈ ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ↔ ∃ z z ∈ ran ⁡ AP ⁡ K ∧ z ∈ 𝒫 F -1 c
26 n0 ⊢ ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅ ↔ ∃ z z ∈ ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c
27 df-rex ⊢ ∃ z ∈ ran ⁡ AP ⁡ K z ∈ 𝒫 F -1 c ↔ ∃ z z ∈ ran ⁡ AP ⁡ K ∧ z ∈ 𝒫 F -1 c
28 25 26 27 3bitr4ri ⊢ ∃ z ∈ ran ⁡ AP ⁡ K z ∈ 𝒫 F -1 c ↔ ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅
29 fveq2 ⊢ w = a d → AP ⁡ K ⁡ w = AP ⁡ K ⁡ a d
30 df-ov ⊢ a AP ⁡ K d = AP ⁡ K ⁡ a d
31 29 30 eqtr4di ⊢ w = a d → AP ⁡ K ⁡ w = a AP ⁡ K d
32 31 sseq1d ⊢ w = a d → AP ⁡ K ⁡ w ⊆ F -1 c ↔ a AP ⁡ K d ⊆ F -1 c
33 32 rexxp ⊢ ∃ w ∈ ℕ × ℕ AP ⁡ K ⁡ w ⊆ F -1 c ↔ ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
34 23 28 33 3bitr3g ⊢ φ → ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅ ↔ ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
35 34 exbidv ⊢ φ → ∃ c ran ⁡ AP ⁡ K ∩ 𝒫 F -1 c ≠ ∅ ↔ ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
36 16 35 bitrd ⊢ φ → K MonoAP F ↔ ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c