α : Type ?u.302906
β : Type ?u.302909
γ : Type ?u.302912
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Sort u_1
f : ι → Cardinal
hf : BddAbove (range f)
⊢ ord (sSup (range f)) = sSup (range fun i => ord (f i))
α : Type ?u.302906
β : Type ?u.302909
γ : Type ?u.302912
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Sort u_1
f : ι → Cardinal
hf : BddAbove (range f)
⊢ ord (iSup f) = ⨆ (i : ι), ord (f i)
unfold iSup
case h.e'_3.h.e'_3
α : Type ?u.302906
β : Type ?u.302909
γ : Type ?u.302912
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Sort u_1
f : ι → Cardinal
hf : BddAbove (range f)
⊢ (range fun i => ord (f i)) = ord '' range f
α : Type ?u.302906
β : Type ?u.302909
γ : Type ?u.302912
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Sort u_1
f : ι → Cardinal
hf : BddAbove (range f)
⊢ ord (sSup (range f)) = sSup (range fun i => ord (f i))
convert sSup_ord hf
case h.e'_3.h.e'_3
α : Type ?u.302906
β : Type ?u.302909
γ : Type ?u.302912
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Sort u_1
f : ι → Cardinal
hf : BddAbove (range f)
⊢ range (ord ∘ f) = ord '' range f
case h.e'_3.h.e'_3
α : Type ?u.302906
β : Type ?u.302909
γ : Type ?u.302912
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Sort u_1
f : ι → Cardinal
hf : BddAbove (range f)
⊢ (range fun i => ord (f i)) = ord '' range f
conv_lhs => change range (ord ∘ f)
no goals
case h.e'_3.h.e'_3
α : Type ?u.302906
β : Type ?u.302909
γ : Type ?u.302912
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Sort u_1
f : ι → Cardinal
hf : BddAbove (range f)
⊢ range (ord ∘ f) = ord '' range f
rw [range_comp]