no goals
α : Type u_3
β : Type ?u.112020
γ : Type ?u.112023
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
o : Ordinal
H : IsNormal f
p : Set α
p0 : Set.Nonempty p
g : α → Ordinal
b : Ordinal
H₂ : ∀ (o : Ordinal), b ≤ o ↔ ∀ (a : α), a ∈ p → g a ≤ o
⊢ f b ≤ o ↔ ∀ (a : α), a ∈ p → f (g a) ≤ o
simpa [H₂] using H.le_set (g '' p) (p0.image g) b