case tfae_1_to_2
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
⊢ a ∈ closure s → a ∈ closure (s ∩ Iic a)

s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
tfae_have 1 → 2
case tfae_2_to_3
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
⊢ a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a

s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
tfae_have 2 → 3
case tfae_3_to_4
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a

s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
tfae_have 3 → 4
case tfae_4_to_5
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
⊢ (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a

s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
tfae_have 4 → 5
case tfae_5_to_6
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
⊢ (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a

s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
tfae_have 5 → 6
case tfae_6_to_1
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) → a ∈ closure s

s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
tfae_6_to_1 : (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) → a ∈ closure s
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
tfae_have 6 → 1
no goals
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
tfae_6_to_1 : (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) → a ∈ closure s
⊢ TFAE
    [a ∈ closure s, a ∈ closure (s ∩ Iic a), Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a,
      ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a,
      ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a,
      ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a]
tfae_finish
case tfae_1_to_2
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
⊢ Filter.NeBot (𝓝[s] a) → Filter.NeBot (𝓝 a ⊓ Filter.principal s)
case tfae_1_to_2
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
⊢ a ∈ closure s → a ∈ closure (s ∩ Iic a)
simp only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter', nhds_left_eq_nhds]
no goals
case tfae_1_to_2
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
⊢ Filter.NeBot (𝓝[s] a) → Filter.NeBot (𝓝 a ⊓ Filter.principal s)
exact id
case tfae_2_to_3
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
case tfae_2_to_3
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
⊢ a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
intro h
case tfae_2_to_3.inl
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
he : s ∩ Iic a = ∅
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a

case tfae_2_to_3.inr
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
hne : Set.Nonempty (s ∩ Iic a)
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
case tfae_2_to_3
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
cases' (s ∩ Iic a).eq_empty_or_nonempty with he hne
no goals
case tfae_2_to_3.inl
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
he : s ∩ Iic a = ∅
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
simp [he] at h
case tfae_2_to_3.inr
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
hne : Set.Nonempty (s ∩ Iic a)
⊢ a ∈ upperBounds (s ∩ Iic a)
case tfae_2_to_3.inr
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
hne : Set.Nonempty (s ∩ Iic a)
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
refine ⟨hne, (isLUB_of_mem_closure ?_ h).csSup_eq hne⟩
no goals
case tfae_2_to_3.inr
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a)
hne : Set.Nonempty (s ∩ Iic a)
⊢ a ∈ upperBounds (s ∩ Iic a)
exact fun x hx => hx.2
no goals
case tfae_3_to_4
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
⊢ Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
exact fun h => ⟨_, inter_subset_left _ _, h.1, bddAbove_Iic.mono (inter_subset_right _ _), h.2⟩
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
case tfae_4_to_5
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
⊢ (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
rintro ⟨t, hts, hne, hbdd, rfl⟩
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
have hlub : IsLUB t (sSup t) := isLUB_csSup hne hbdd
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
let ⟨y, hyt⟩ := hne
case tfae_4_to_5.intro.intro.intro.intro.refine_1
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
x✝ : x < succ (sSup t)
⊢ (fun x x_1 => if x ∈ t then x else y) x x✝ ∈ s

case tfae_4_to_5.intro.intro.intro.intro.refine_2
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
⊢ (bsup (succ (sSup t)) fun x x_1 => if x ∈ t then x else y) = sSup t
case tfae_4_to_5.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
⊢ ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = sSup t
refine ⟨succ (sSup t), succ_ne_zero _, fun x _ => if x ∈ t then x else y, fun x _ => ?_, ?_⟩
case tfae_4_to_5.intro.intro.intro.intro.refine_1
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
x✝ : x < succ (sSup t)
⊢ (if x ∈ t then x else y) ∈ s
case tfae_4_to_5.intro.intro.intro.intro.refine_1
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
x✝ : x < succ (sSup t)
⊢ (fun x x_1 => if x ∈ t then x else y) x x✝ ∈ s
simp only
no goals
case tfae_4_to_5.intro.intro.intro.intro.refine_1
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
x✝ : x < succ (sSup t)
⊢ (if x ∈ t then x else y) ∈ s
split_ifs with h <;> exact hts ‹_›
case tfae_4_to_5.intro.intro.intro.intro.refine_2.refine_1
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
x✝ : x < succ (sSup t)
⊢ (if x ∈ t then x else y) ≤ sSup t

case tfae_4_to_5.intro.intro.intro.intro.refine_2.refine_2
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
hx : x ∈ t
⊢ x ≤ bsup (succ (sSup t)) fun x x_1 => if x ∈ t then x else y
case tfae_4_to_5.intro.intro.intro.intro.refine_2
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
⊢ (bsup (succ (sSup t)) fun x x_1 => if x ∈ t then x else y) = sSup t
refine le_antisymm (bsup_le fun x _ => ?_) (csSup_le hne fun x hx => ?_)
no goals
case tfae_4_to_5.intro.intro.intro.intro.refine_2.refine_1
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
x✝ : x < succ (sSup t)
⊢ (if x ∈ t then x else y) ≤ sSup t
split_ifs <;> exact hlub.1 ‹_›
no goals
case tfae_4_to_5.intro.intro.intro.intro.refine_2.refine_2
s✝ : Set Ordinal
a : Ordinal
s t : Set Ordinal
hts : t ⊆ s
hne : Set.Nonempty t
hbdd : BddAbove t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sSup t)) ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1, t_1 ⊆ s ∧ Set.Nonempty t_1 ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
hlub : IsLUB t (sSup t)
y : Ordinal
hyt : y ∈ t
x : Ordinal
hx : x ∈ t
⊢ x ≤ bsup (succ (sSup t)) fun x x_1 => if x ∈ t then x else y
refine (if_pos hx).symm.trans_le (le_bsup _ _ <| (hlub.1 hx).trans_lt (lt_succ _))
case tfae_5_to_6.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s : Set Ordinal
o : Ordinal
h₀ : o ≠ 0
f : (x : Ordinal) → x < o → Ordinal
hfs : ∀ (x : Ordinal) (hx : x < o), f x hx ∈ s
tfae_1_to_2 : bsup o f ∈ closure s → bsup o f ∈ closure (s ∩ Iic (bsup o f))
tfae_2_to_3 :
  bsup o f ∈ closure (s ∩ Iic (bsup o f)) → Set.Nonempty (s ∩ Iic (bsup o f)) ∧ sSup (s ∩ Iic (bsup o f)) = bsup o f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (bsup o f)) ∧ sSup (s ∩ Iic (bsup o f)) = bsup o f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = bsup o f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = bsup o f) →
    ∃ o_1, o_1 ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o_1), f_1 x hx ∈ s) ∧ bsup o_1 f_1 = bsup o f
⊢ ∃ ι, Nonempty ι ∧ ∃ f_1, (∀ (i : ι), f_1 i ∈ s) ∧ sup f_1 = bsup o f
case tfae_5_to_6
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
⊢ (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
rintro ⟨o, h₀, f, hfs, rfl⟩
no goals
case tfae_5_to_6.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s : Set Ordinal
o : Ordinal
h₀ : o ≠ 0
f : (x : Ordinal) → x < o → Ordinal
hfs : ∀ (x : Ordinal) (hx : x < o), f x hx ∈ s
tfae_1_to_2 : bsup o f ∈ closure s → bsup o f ∈ closure (s ∩ Iic (bsup o f))
tfae_2_to_3 :
  bsup o f ∈ closure (s ∩ Iic (bsup o f)) → Set.Nonempty (s ∩ Iic (bsup o f)) ∧ sSup (s ∩ Iic (bsup o f)) = bsup o f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (bsup o f)) ∧ sSup (s ∩ Iic (bsup o f)) = bsup o f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = bsup o f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = bsup o f) →
    ∃ o_1, o_1 ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o_1), f_1 x hx ∈ s) ∧ bsup o_1 f_1 = bsup o f
⊢ ∃ ι, Nonempty ι ∧ ∃ f_1, (∀ (i : ι), f_1 i ∈ s) ∧ sup f_1 = bsup o f
exact ⟨_, out_nonempty_iff_ne_zero.2 h₀, familyOfBFamily o f, fun _ => hfs _ _, rfl⟩
case tfae_6_to_1.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s : Set Ordinal
ι : Type u
hne : Nonempty ι
f : ι → Ordinal
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : sup f ∈ closure s → sup f ∈ closure (s ∩ Iic (sup f))
tfae_2_to_3 : sup f ∈ closure (s ∩ Iic (sup f)) → Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ sup f_1 = sup f
⊢ sup f ∈ closure s
case tfae_6_to_1
s✝ : Set Ordinal
a✝ a : Ordinal
s : Set Ordinal
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : Set.Nonempty (s ∩ Iic a) ∧ sSup (s ∩ Iic a) = a → ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = a) →
    ∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal) (hx : x < o), f x hx ∈ s) ∧ bsup o f = a) →
    ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a) → a ∈ closure s
rintro ⟨ι, hne, f, hfs, rfl⟩
case tfae_6_to_1.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s : Set Ordinal
ι : Type u
hne : Nonempty ι
f : ι → Ordinal
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : sup f ∈ closure s → sup f ∈ closure (s ∩ Iic (sup f))
tfae_2_to_3 : sup f ∈ closure (s ∩ Iic (sup f)) → Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ sup f_1 = sup f
⊢ sSup (Set.range f) ∈ closure s
case tfae_6_to_1.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s : Set Ordinal
ι : Type u
hne : Nonempty ι
f : ι → Ordinal
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : sup f ∈ closure s → sup f ∈ closure (s ∩ Iic (sup f))
tfae_2_to_3 : sup f ∈ closure (s ∩ Iic (sup f)) → Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ sup f_1 = sup f
⊢ sup f ∈ closure s
rw [sup, iSup]
no goals
case tfae_6_to_1.intro.intro.intro.intro
s✝ : Set Ordinal
a : Ordinal
s : Set Ordinal
ι : Type u
hne : Nonempty ι
f : ι → Ordinal
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : sup f ∈ closure s → sup f ∈ closure (s ∩ Iic (sup f))
tfae_2_to_3 : sup f ∈ closure (s ∩ Iic (sup f)) → Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f
tfae_3_to_4 :
  Set.Nonempty (s ∩ Iic (sup f)) ∧ sSup (s ∩ Iic (sup f)) = sup f →
    ∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f
tfae_4_to_5 :
  (∃ t, t ⊆ s ∧ Set.Nonempty t ∧ BddAbove t ∧ sSup t = sup f) →
    ∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f
tfae_5_to_6 :
  (∃ o, o ≠ 0 ∧ ∃ f_1, (∀ (x : Ordinal) (hx : x < o), f_1 x hx ∈ s) ∧ bsup o f_1 = sup f) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ sup f_1 = sup f
⊢ sSup (Set.range f) ∈ closure s
exact closure_mono (range_subset_iff.2 hfs) <| csSup_mem_closure (range_nonempty f)
  (bddAbove_range.{u, u} f)