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 ⊢ 𝑋 ∈ V
vdwmc.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
vdwmc.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑅 )
Assertion vdwmc ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )

Proof

Step Hyp Ref Expression
1 vdwmc.1 ⊢ 𝑋 ∈ V
2 vdwmc.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 vdwmc.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑅 )
4 fex ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑅 ∧ 𝑋 ∈ V ) → 𝐹 ∈ V )
5 3 1 4 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( AP ‘ 𝑘 ) = ( AP ‘ 𝐾 ) )
7 6 rneqd ⊢ ( 𝑘 = 𝐾 → ran ( AP ‘ 𝑘 ) = ran ( AP ‘ 𝐾 ) )
8 cnveq ⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
9 8 imaeq1d ⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ { 𝑐 } ) = ( ◡ 𝐹 “ { 𝑐 } ) )
10 9 pweqd ⊢ ( 𝑓 = 𝐹 → 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) = 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) )
11 7 10 ineqan12d ⊢ ( ( 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) = ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) )
12 11 neeq1d ⊢ ( ( 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) ≠ ∅ ↔ ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ ) )
13 12 exbidv ⊢ ( ( 𝑘 = 𝐾 ∧ 𝑓 = 𝐹 ) → ( ∃ 𝑐 ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) ≠ ∅ ↔ ∃ 𝑐 ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ ) )
14 df-vdwmc ⊢ MonoAP = { ⟨ 𝑘 , 𝑓 ⟩ ∣ ∃ 𝑐 ( ran ( AP ‘ 𝑘 ) ∩ 𝒫 ( ◡ 𝑓 “ { 𝑐 } ) ) ≠ ∅ }
15 13 14 brabga ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐹 ∈ V ) → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ ) )
16 2 5 15 syl2anc ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ ) )
17 vdwapf ⊢ ( 𝐾 ∈ ℕ0 → ( AP ‘ 𝐾 ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ )
18 ffn ⊢ ( ( AP ‘ 𝐾 ) : ( ℕ × ℕ ) ⟶ 𝒫 ℕ → ( AP ‘ 𝐾 ) Fn ( ℕ × ℕ ) )
19 velpw ⊢ ( 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ↔ 𝑧 ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
20 sseq1 ⊢ ( 𝑧 = ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) → ( 𝑧 ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
21 19 20 bitrid ⊢ ( 𝑧 = ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) → ( 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
22 21 rexrn ⊢ ( ( AP ‘ 𝐾 ) Fn ( ℕ × ℕ ) → ( ∃ 𝑧 ∈ ran ( AP ‘ 𝐾 ) 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑤 ∈ ( ℕ × ℕ ) ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
23 2 17 18 22 4syl ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ran ( AP ‘ 𝐾 ) 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑤 ∈ ( ℕ × ℕ ) ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
24 elin ⊢ ( 𝑧 ∈ ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ( 𝑧 ∈ ran ( AP ‘ 𝐾 ) ∧ 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) )
25 24 exbii ⊢ ( ∃ 𝑧 𝑧 ∈ ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ ran ( AP ‘ 𝐾 ) ∧ 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) )
26 n0 ⊢ ( ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) )
27 df-rex ⊢ ( ∃ 𝑧 ∈ ran ( AP ‘ 𝐾 ) 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑧 ( 𝑧 ∈ ran ( AP ‘ 𝐾 ) ∧ 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) )
28 25 26 27 3bitr4ri ⊢ ( ∃ 𝑧 ∈ ran ( AP ‘ 𝐾 ) 𝑧 ∈ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ )
29 fveq2 ⊢ ( 𝑤 = ⟨ 𝑎 , 𝑑 ⟩ → ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) = ( ( AP ‘ 𝐾 ) ‘ ⟨ 𝑎 , 𝑑 ⟩ ) )
30 df-ov ⊢ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) = ( ( AP ‘ 𝐾 ) ‘ ⟨ 𝑎 , 𝑑 ⟩ )
31 29 30 eqtr4di ⊢ ( 𝑤 = ⟨ 𝑎 , 𝑑 ⟩ → ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) = ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) )
32 31 sseq1d ⊢ ( 𝑤 = ⟨ 𝑎 , 𝑑 ⟩ → ( ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
33 32 rexxp ⊢ ( ∃ 𝑤 ∈ ( ℕ × ℕ ) ( ( AP ‘ 𝐾 ) ‘ 𝑤 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
34 23 28 33 3bitr3g ⊢ ( 𝜑 → ( ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
35 34 exbidv ⊢ ( 𝜑 → ( ∃ 𝑐 ( ran ( AP ‘ 𝐾 ) ∩ 𝒫 ( ◡ 𝐹 “ { 𝑐 } ) ) ≠ ∅ ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
36 16 35 bitrd ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )