o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
⊢ (¬∃ i hi, nfpBFamily o f a ≤ f i hi b) ↔ ¬nfpBFamily o f a ≤ b
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
⊢ (∃ i hi, nfpBFamily o f a ≤ f i hi b) ↔ nfpBFamily o f a ≤ b
rw [← not_iff_not]
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
⊢ (∀ (i : Ordinal) (hi : i < o), f i hi b < nfpBFamily o f a) ↔ b < nfpBFamily o f a
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
⊢ (¬∃ i hi, nfpBFamily o f a ≤ f i hi b) ↔ ¬nfpBFamily o f a ≤ b
push_neg
no goals
o : Ordinal
f : (b : Ordinal) → b < o → Ordinal → Ordinal
ho : o ≠ 0
H : ∀ (i : Ordinal) (hi : i < o), IsNormal (f i hi)
a : Ordinal
b : Ordinal
⊢ (∀ (i : Ordinal) (hi : i < o), f i hi b < nfpBFamily o f a) ↔ b < nfpBFamily o f a
exact apply_lt_nfpBFamily_iff.{u, v} ho H