α : Type ?u.161838
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
ha : a < ord c
⊢ ℵ₀ < c

α : Type ?u.161838
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
ha : a < ord c
⊢ lift (#ι) < c
α : Type ?u.161838
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
ha : a < ord c
⊢ nfpFamily f a < ord c
apply nfpFamily_lt_ord_lift.{u, v} _ _ hf ha <;> rw [hc.cof_eq]
α : Type ?u.161838
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
ha : a < ord c
⊢ lift (#ι) < c
α : Type ?u.161838
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
ha : a < ord c
⊢ ℵ₀ < c

α : Type ?u.161838
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
ha : a < ord c
⊢ lift (#ι) < c
exact lt_of_le_of_ne hc.1 hc'.symm
no goals
α : Type ?u.161838
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
ha : a < ord c
⊢ lift (#ι) < c
exact hι