Metamath Proof Explorer

Theorem rami

Description: The defining property of a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypotheses rami.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
rami.m ⊢ φ → M ∈ ℕ 0
rami.r ⊢ φ → R ∈ V
rami.f ⊢ φ → F : R ⟶ ℕ 0
rami.x ⊢ φ → M Ramsey F ∈ ℕ 0
rami.s ⊢ φ → S ∈ W
rami.l ⊢ φ → M Ramsey F ≤ S
rami.g ⊢ φ → G : S C M ⟶ R
Assertion rami ⊢ φ → ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ G -1 c

Proof

Step Hyp Ref Expression
1 rami.c ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 rami.m ⊢ φ → M ∈ ℕ 0
3 rami.r ⊢ φ → R ∈ V
4 rami.f ⊢ φ → F : R ⟶ ℕ 0
5 rami.x ⊢ φ → M Ramsey F ∈ ℕ 0
6 rami.s ⊢ φ → S ∈ W
7 rami.l ⊢ φ → M Ramsey F ≤ S
8 rami.g ⊢ φ → G : S C M ⟶ R
9 cnveq ⊢ f = G → f -1 = G -1
10 9 imaeq1d ⊢ f = G → f -1 c = G -1 c
11 10 sseq2d ⊢ f = G → x C M ⊆ f -1 c ↔ x C M ⊆ G -1 c
12 11 anbi2d ⊢ f = G → F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ F ⁡ c ≤ x ∧ x C M ⊆ G -1 c
13 12 2rexbidv ⊢ f = G → ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ G -1 c
14 eqid ⊢ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c = n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
15 1 14 ramtcl2 ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ↔ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ≠ ∅
16 1 14 ramtcl ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ≠ ∅
17 15 16 bitr4d ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 → M Ramsey F ∈ ℕ 0 ↔ M Ramsey F ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
18 2 3 4 17 syl3anc ⊢ φ → M Ramsey F ∈ ℕ 0 ↔ M Ramsey F ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
19 5 18 mpbid ⊢ φ → M Ramsey F ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
20 breq1 ⊢ n = M Ramsey F → n ≤ s ↔ M Ramsey F ≤ s
21 20 imbi1d ⊢ n = M Ramsey F → n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ M Ramsey F ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
22 21 albidv ⊢ n = M Ramsey F → ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ ∀ s M Ramsey F ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
23 22 elrab ⊢ M Ramsey F ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ M Ramsey F ∈ ℕ 0 ∧ ∀ s M Ramsey F ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
24 23 simprbi ⊢ M Ramsey F ∈ n ∈ ℕ 0 | ∀ s n ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c → ∀ s M Ramsey F ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
25 19 24 syl ⊢ φ → ∀ s M Ramsey F ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
26 fveq2 ⊢ s = S → s = S
27 26 breq2d ⊢ s = S → M Ramsey F ≤ s ↔ M Ramsey F ≤ S
28 oveq1 ⊢ s = S → s C M = S C M
29 28 oveq2d ⊢ s = S → R s C M = R S C M
30 pweq ⊢ s = S → 𝒫 s = 𝒫 S
31 30 rexeqdv ⊢ s = S → ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
32 31 rexbidv ⊢ s = S → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
33 29 32 raleqbidv ⊢ s = S → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ ∀ f ∈ R S C M ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
34 27 33 imbi12d ⊢ s = S → M Ramsey F ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c ↔ M Ramsey F ≤ S → ∀ f ∈ R S C M ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
35 34 spcgv ⊢ S ∈ W → ∀ s M Ramsey F ≤ s → ∀ f ∈ R s C M ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x C M ⊆ f -1 c → M Ramsey F ≤ S → ∀ f ∈ R S C M ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
36 6 25 7 35 syl3c ⊢ φ → ∀ f ∈ R S C M ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ f -1 c
37 ovex ⊢ S C M ∈ V
38 elmapg ⊢ R ∈ V ∧ S C M ∈ V → G ∈ R S C M ↔ G : S C M ⟶ R
39 3 37 38 sylancl ⊢ φ → G ∈ R S C M ↔ G : S C M ⟶ R
40 8 39 mpbird ⊢ φ → G ∈ R S C M
41 13 36 40 rspcdva ⊢ φ → ∃ c ∈ R ∃ x ∈ 𝒫 S F ⁡ c ≤ x ∧ x C M ⊆ G -1 c