S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o : Ordinal
⊢ ∀ (j : Ordinal), (∀ (k : Ordinal), k < j → enumOrd (range f) k = f k) → enumOrd (range f) j = f j
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o : Ordinal
⊢ enumOrd (range f) o = f o
apply Ordinal.induction o
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
⊢ enumOrd (range f) a = f a
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o : Ordinal
⊢ ∀ (j : Ordinal), (∀ (k : Ordinal), k < j → enumOrd (range f) k = f k) → enumOrd (range f) j = f j
intro a H
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
⊢ sInf (range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}) = f a
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
⊢ enumOrd (range f) a = f a
rw [enumOrd_def a]
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
⊢ sInf (range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}) = f a
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
⊢ sInf (range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}) = f a
have Hfa : f a ∈ range f ∩ { b | ∀ c, c < a → enumOrd (range f) c < b } :=
  ⟨mem_range_self a, fun b hb => by
    rw [H b hb]
    exact hf hb⟩
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
⊢ ∀ (b : Ordinal), b ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b} → f a ≤ b
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
⊢ sInf (range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}) = f a
refine' (csInf_le' Hfa).antisymm ((le_csInf_iff'' ⟨_, Hfa⟩).2 _)
case intro.intro
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
c : Ordinal
hc : ∀ (b : Ordinal), b < a → enumOrd (range f) b < f c
⊢ f a ≤ f c
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
⊢ ∀ (b : Ordinal), b ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b} → f a ≤ b
rintro _ ⟨⟨c, rfl⟩, hc : ∀ b < a, enumOrd (range f) b < f c⟩
case intro.intro
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
c : Ordinal
hc : ∀ (b : Ordinal), b < a → enumOrd (range f) b < f c
⊢ a ≤ c
case intro.intro
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
c : Ordinal
hc : ∀ (b : Ordinal), b < a → enumOrd (range f) b < f c
⊢ f a ≤ f c
rw [hf.le_iff_le]
case intro.intro
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
c : Ordinal
hc : c < a
⊢ ∃ b, b < a ∧ f c ≤ enumOrd (range f) b
case intro.intro
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
c : Ordinal
hc : ∀ (b : Ordinal), b < a → enumOrd (range f) b < f c
⊢ a ≤ c
contrapose! hc
no goals
case intro.intro
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
Hfa : f a ∈ range f ∩ {b | ∀ (c : Ordinal), c < a → enumOrd (range f) c < b}
c : Ordinal
hc : c < a
⊢ ∃ b, b < a ∧ f c ≤ enumOrd (range f) b
exact ⟨c, hc, (H c hc).ge⟩
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
b : Ordinal
hb : b < a
⊢ f b < f a
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
b : Ordinal
hb : b < a
⊢ enumOrd (range f) b < f a
rw [H b hb]
no goals
S : Set Ordinal
f : Ordinal → Ordinal
hf : StrictMono f
o a : Ordinal
H : ∀ (k : Ordinal), k < a → enumOrd (range f) k = f k
b : Ordinal
hb : b < a
⊢ f b < f a
exact hf hb