Proofgold Proposition

∀ x0 . ∀ x1 x2 x3 : ι → ι . infinite x0 ⟶ (∀ x4 . x4 ⊆ x0 ⟶ infinite x4 ⟶ and (x1 x4 ⊆ x4) (infinite (x1 x4))) ⟶ (∀ x4 . x4 ⊆ x0 ⟶ infinite x4 ⟶ and (x2 x4 ∈ x4) (nIn (x2 x4) (x1 x4))) ⟶ x3 0 = x1 x0 ⟶ (∀ x4 . nat_p x4 ⟶ x3 (ordsucc x4) = x1 (x3 x4)) ⟶ and (and (∀ x4 . nat_p x4 ⟶ and (x3 x4 ⊆ x0) (infinite (x3 x4))) (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ omega ⟶ x4 ⊆ x5 ⟶ x3 x5 ⊆ x3 x4)) (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ omega ⟶ x2 (x3 x4) = x2 (x3 x5) ⟶ x4 = x5)

type
prop

theory
HotG

name
-

proof
PUQQ9..

Megalodon
infiniteRamsey_lem

proofgold address
TMSZa..^{infiniteRamsey_lem}

creator
30111 PrQUS../81fd1..

owner
30111 PrQUS../81fd1..

term root
c8e82..