Theorem vdwmc 15961

Description: The predicate " The ⟨𝑅, 𝑁⟩-coloring 𝐹 contains a monochromatic AP of length 𝐾". (Contributed by Mario Carneiro, 18-Aug-2014.)

Hypotheses

Ref	Expression
vdwmc.1	⊢ 𝑋 ∈ V
vdwmc.2	⊢ (𝜑 → 𝐾 ∈ ℕ0)
vdwmc.3	⊢ (𝜑 → 𝐹:𝑋⟶𝑅)

Assertion

Ref	Expression
vdwmc	⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))

Distinct variable groups:   𝑎,𝑐,𝑑,𝐹   𝐾,𝑎,𝑐,𝑑   𝜑,𝑐

Allowed substitution hints:   𝜑(𝑎,𝑑)   𝑅(𝑎,𝑐,𝑑)   𝑋(𝑎,𝑐,𝑑)

Proof of Theorem vdwmc

Dummy variables 𝑓 𝑘 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vdwmc.2	. . 3 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
2		vdwmc.3	. . . 4 ⊢ (𝜑 → 𝐹:𝑋⟶𝑅)
3		vdwmc.1	. . . 4 ⊢ 𝑋 ∈ V
4		fex 6682	. . . 4 ⊢ ((𝐹:𝑋⟶𝑅 ∧ 𝑋 ∈ V) → 𝐹 ∈ V)
5	2, 3, 4	sylancl 580	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
6		fveq2 6375	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (AP‘𝑘) = (AP‘𝐾))
7	6	rneqd 5521	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ran (AP‘𝑘) = ran (AP‘𝐾))
8		cnveq 5464	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → ◡𝑓 = ◡𝐹)
9	8	imaeq1d 5647	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (◡𝑓 “ {𝑐}) = (◡𝐹 “ {𝑐}))
10	9	pweqd 4320	. . . . . . 7 ⊢ (𝑓 = 𝐹 → 𝒫 (◡𝑓 “ {𝑐}) = 𝒫 (◡𝐹 “ {𝑐}))
11	7, 10	ineqan12d 3978	. . . . . 6 ⊢ ((𝑘 = 𝐾 ∧ 𝑓 = 𝐹) → (ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) = (ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})))
12	11	neeq1d 2996	. . . . 5 ⊢ ((𝑘 = 𝐾 ∧ 𝑓 = 𝐹) → ((ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅ ↔ (ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅))
13	12	exbidv 2016	. . . 4 ⊢ ((𝑘 = 𝐾 ∧ 𝑓 = 𝐹) → (∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅ ↔ ∃𝑐(ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅))
14		df-vdwmc 15952	. . . 4 ⊢ MonoAP = {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅}
15	13, 14	brabga 5150	. . 3 ⊢ ((𝐾 ∈ ℕ0 ∧ 𝐹 ∈ V) → (𝐾 MonoAP 𝐹 ↔ ∃𝑐(ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅))
16	1, 5, 15	syl2anc 579	. 2 ⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐(ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅))
17		vdwapf 15955	. . . . 5 ⊢ (𝐾 ∈ ℕ0 → (AP‘𝐾):(ℕ × ℕ)⟶𝒫 ℕ)
18		ffn 6223	. . . . 5 ⊢ ((AP‘𝐾):(ℕ × ℕ)⟶𝒫 ℕ → (AP‘𝐾) Fn (ℕ × ℕ))
19		selpw 4322	. . . . . . 7 ⊢ (𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐}) ↔ 𝑧 ⊆ (◡𝐹 “ {𝑐}))
20		sseq1 3786	. . . . . . 7 ⊢ (𝑧 = ((AP‘𝐾)‘𝑤) → (𝑧 ⊆ (◡𝐹 “ {𝑐}) ↔ ((AP‘𝐾)‘𝑤) ⊆ (◡𝐹 “ {𝑐})))
21	19, 20	syl5bb 274	. . . . . 6 ⊢ (𝑧 = ((AP‘𝐾)‘𝑤) → (𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐}) ↔ ((AP‘𝐾)‘𝑤) ⊆ (◡𝐹 “ {𝑐})))
22	21	rexrn 6551	. . . . 5 ⊢ ((AP‘𝐾) Fn (ℕ × ℕ) → (∃𝑧 ∈ ran (AP‘𝐾)𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐}) ↔ ∃𝑤 ∈ (ℕ × ℕ)((AP‘𝐾)‘𝑤) ⊆ (◡𝐹 “ {𝑐})))
23	1, 17, 18, 22	4syl 19	. . . 4 ⊢ (𝜑 → (∃𝑧 ∈ ran (AP‘𝐾)𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐}) ↔ ∃𝑤 ∈ (ℕ × ℕ)((AP‘𝐾)‘𝑤) ⊆ (◡𝐹 “ {𝑐})))
24		elin 3958	. . . . . 6 ⊢ (𝑧 ∈ (ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ↔ (𝑧 ∈ ran (AP‘𝐾) ∧ 𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐})))
25	24	exbii 1943	. . . . 5 ⊢ (∃𝑧 𝑧 ∈ (ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ↔ ∃𝑧(𝑧 ∈ ran (AP‘𝐾) ∧ 𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐})))
26		n0 4095	. . . . 5 ⊢ ((ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})))
27		df-rex 3061	. . . . 5 ⊢ (∃𝑧 ∈ ran (AP‘𝐾)𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐}) ↔ ∃𝑧(𝑧 ∈ ran (AP‘𝐾) ∧ 𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐})))
28	25, 26, 27	3bitr4ri 295	. . . 4 ⊢ (∃𝑧 ∈ ran (AP‘𝐾)𝑧 ∈ 𝒫 (◡𝐹 “ {𝑐}) ↔ (ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅)
29		fveq2 6375	. . . . . . 7 ⊢ (𝑤 = ⟨𝑎, 𝑑⟩ → ((AP‘𝐾)‘𝑤) = ((AP‘𝐾)‘⟨𝑎, 𝑑⟩))
30		df-ov 6845	. . . . . . 7 ⊢ (𝑎(AP‘𝐾)𝑑) = ((AP‘𝐾)‘⟨𝑎, 𝑑⟩)
31	29, 30	syl6eqr 2817	. . . . . 6 ⊢ (𝑤 = ⟨𝑎, 𝑑⟩ → ((AP‘𝐾)‘𝑤) = (𝑎(AP‘𝐾)𝑑))
32	31	sseq1d 3792	. . . . 5 ⊢ (𝑤 = ⟨𝑎, 𝑑⟩ → (((AP‘𝐾)‘𝑤) ⊆ (◡𝐹 “ {𝑐}) ↔ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))
33	32	rexxp 5433	. . . 4 ⊢ (∃𝑤 ∈ (ℕ × ℕ)((AP‘𝐾)‘𝑤) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))
34	23, 28, 33	3bitr3g 304	. . 3 ⊢ (𝜑 → ((ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅ ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))
35	34	exbidv 2016	. 2 ⊢ (𝜑 → (∃𝑐(ran (AP‘𝐾) ∩ 𝒫 (◡𝐹 “ {𝑐})) ≠ ∅ ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))
36	16, 35	bitrd 270	1 ⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1652  ∃wex 1874   ∈ wcel 2155   ≠ wne 2937  ∃wrex 3056  Vcvv 3350   ∩ cin 3731   ⊆ wss 3732  ∅c0 4079  𝒫 cpw 4315  {csn 4334  ⟨cop 4340   class class class wbr 4809   × cxp 5275  ^◡ccnv 5276  ran crn 5278   “ cima 5280   Fn wfn 6063  ⟶wf 6064  ‘cfv 6068  (class class class)co 6842  ℕcn 11274  ℕ₀cn0 11538  APcvdwa 15948   MonoAP cvdwm 15949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-vdwap 15951  df-vdwmc 15952

This theorem is referenced by:  vdwmc2  15962  vdwlem1  15964  vdwlem2  15965  vdwlem9  15972  vdwlem10  15973  vdwlem12  15975  vdwlem13  15976