α β : Type u
s : Set Cardinal
hs : BddAbove s
⊢ ∀ (c : Cardinal), c ∈ upperBounds (lift '' s) → lift (sSup s) ≤ c

α β : Type u
s : Set Cardinal
hs : BddAbove s
⊢ lift (sSup s) ∈ upperBounds (lift '' s)
α β : Type u
s : Set Cardinal
hs : BddAbove s
⊢ lift (sSup s) = sSup (lift '' s)
apply ((le_csSup_iff' (bddAbove_image.{_,u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
α β : Type u
s : Set Cardinal
hs : BddAbove s
c : Cardinal
hc : c ∈ upperBounds (lift '' s)
⊢ lift (sSup s) ≤ c
α β : Type u
s : Set Cardinal
hs : BddAbove s
⊢ ∀ (c : Cardinal), c ∈ upperBounds (lift '' s) → lift (sSup s) ≤ c
intro c hc
α β : Type u
s : Set Cardinal
hs : BddAbove s
c : Cardinal
hc : c ∈ upperBounds (lift '' s)
h : ¬lift (sSup s) ≤ c
⊢ False
α β : Type u
s : Set Cardinal
hs : BddAbove s
c : Cardinal
hc : c ∈ upperBounds (lift '' s)
⊢ lift (sSup s) ≤ c
by_contra h
case intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
d : Cardinal
hc : lift d ∈ upperBounds (lift '' s)
h : ¬lift (sSup s) ≤ lift d
⊢ False
α β : Type u
s : Set Cardinal
hs : BddAbove s
c : Cardinal
hc : c ∈ upperBounds (lift '' s)
h : ¬lift (sSup s) ≤ c
⊢ False
obtain ⟨d, rfl⟩ := Cardinal.lift_down (not_le.1 h).le
case intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
d : Cardinal
hc : lift d ∈ upperBounds (lift '' s)
h : ¬sSup s ≤ d
⊢ False
case intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
d : Cardinal
hc : lift d ∈ upperBounds (lift '' s)
h : ¬lift (sSup s) ≤ lift d
⊢ False
simp_rw [lift_le] at h hc
case intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
d : Cardinal
hc : lift d ∈ upperBounds (lift '' s)
h : ¬∀ (x : Cardinal), x ∈ s → x ≤ d
⊢ False
case intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
d : Cardinal
hc : lift d ∈ upperBounds (lift '' s)
h : ¬sSup s ≤ d
⊢ False
rw [csSup_le_iff' hs] at h
no goals
case intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
d : Cardinal
hc : lift d ∈ upperBounds (lift '' s)
h : ¬∀ (x : Cardinal), x ∈ s → x ≤ d
⊢ False
exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)
case intro.intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
j : Cardinal
hj : j ∈ s
⊢ lift j ≤ lift (sSup s)
α β : Type u
s : Set Cardinal
hs : BddAbove s
⊢ lift (sSup s) ∈ upperBounds (lift '' s)
rintro i ⟨j, hj, rfl⟩
no goals
case intro.intro
α β : Type u
s : Set Cardinal
hs : BddAbove s
j : Cardinal
hj : j ∈ s
⊢ lift j ≤ lift (sSup s)
exact lift_le.2 (le_csSup hs hj)