Proof Summary of Ordinal_Arithmetic.thy:1235

Isabelle Statement

source: Ordinal_Arithmetic.thy:1235 benchmark: isa/deeper/B-mesh-th0/train2k problem: problems/HOL-Cardinals/0009_Ordinal_Arithmetic/prob_01235_053796.p

Lemma

1220
1221
1222

lemma oexp_monoR:
  assumes "oone <o r" "s <o t"
  shows   "r ^o s <o r ^o t" (is "?L <o ?R")

Proof Excerpt

have "Field r ≠ {}" by (metis assms(1) internalize_ordLess not_psubset_empty)
moreover
{ assume "Field r = {r.zero}"
  hence "r = {(r.zero, r.zero)}" using refl_onD[OF r.REFL, of r.zero] unfolding Field_def by auto
  hence "r =o oone" by (metis oone_ordIso ordIso_symmetric)
  with not_ordLess_ordIso[OF assms(1)] have False by (metis ordIso_symmetric)

Conjectures

None

Axioms

c_0_0 c_0_1 c_0_2

Final Contradiction

c_0_14