Metamath Proof Explorer

Theorem ramcl2

Description: The Ramsey number is either a nonnegative integer or plus infinity. (Contributed by Mario Carneiro, 20-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Assertion ramcl2 ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0→MRamseyF∈ℕ0∪+∞

Proof

Step Hyp Ref Expression
1 eqid ⊢a∈V,i∈ℕ0⟼b∈𝒫a|b=i=a∈V,i∈ℕ0⟼b∈𝒫a|b=i
2 eqid ⊢n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c=n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c
3 1 2 ramcl2lem ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0→MRamseyF=ifn∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c=∅+∞supn∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1cℝ<
4 iftrue ⊢n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c=∅→ifn∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c=∅+∞supn∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1cℝ<=+∞
5 3 4 sylan9eq ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0∧n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c=∅→MRamseyF=+∞
6 ssun2 ⊢+∞⊆ℕ0∪+∞
7 pnfex ⊢+∞∈V
8 7 snss ⊢+∞∈ℕ0∪+∞↔+∞⊆ℕ0∪+∞
9 6 8 mpbir ⊢+∞∈ℕ0∪+∞
10 5 9 eqeltrdi ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0∧n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c=∅→MRamseyF∈ℕ0∪+∞
11 ssun1 ⊢ℕ0⊆ℕ0∪+∞
12 1 2 ramtcl2 ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0→MRamseyF∈ℕ0↔n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c≠∅
13 12 biimpar ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0∧n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c≠∅→MRamseyF∈ℕ0
14 11 13 sselid ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0∧n∈ℕ0|∀sn≤s→∀f∈Rsa∈V,i∈ℕ0⟼b∈𝒫a|b=iM∃c∈R∃x∈𝒫sF⁡c≤x∧xa∈V,i∈ℕ0⟼b∈𝒫a|b=iM⊆f-1c≠∅→MRamseyF∈ℕ0∪+∞
15 10 14 pm2.61dane ⊢M∈ℕ0∧R∈V∧F:R⟶ℕ0→MRamseyF∈ℕ0∪+∞