Metamath Proof Explorer

Theorem dflim7

Description: A limit ordinal is a non-zero ordinal that contains all the successors of its elements. Lemma 1.18 of Schloeder p. 2. Closely related to dflim4 . (Contributed by RP, 17-Jan-2025)

Ref Expression
Assertion dflim7 
|- ( Lim A <-> ( Ord A /\ A. b e. A suc b e. A /\ A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 dflim4 
 |-  ( Lim A <-> ( Ord A /\ (/) e. A /\ A. b e. A suc b e. A ) )
2 ord0eln0 
 |-  ( Ord A -> ( (/) e. A <-> A =/= (/) ) )
3 2 anbi1d 
 |-  ( Ord A -> ( ( (/) e. A /\ A. b e. A suc b e. A ) <-> ( A =/= (/) /\ A. b e. A suc b e. A ) ) )
4 3 biancomd 
 |-  ( Ord A -> ( ( (/) e. A /\ A. b e. A suc b e. A ) <-> ( A. b e. A suc b e. A /\ A =/= (/) ) ) )
5 4 pm5.32i 
 |-  ( ( Ord A /\ ( (/) e. A /\ A. b e. A suc b e. A ) ) <-> ( Ord A /\ ( A. b e. A suc b e. A /\ A =/= (/) ) ) )
6 3anass 
 |-  ( ( Ord A /\ (/) e. A /\ A. b e. A suc b e. A ) <-> ( Ord A /\ ( (/) e. A /\ A. b e. A suc b e. A ) ) )
7 3anass 
 |-  ( ( Ord A /\ A. b e. A suc b e. A /\ A =/= (/) ) <-> ( Ord A /\ ( A. b e. A suc b e. A /\ A =/= (/) ) ) )
8 5 6 7 3bitr4i 
 |-  ( ( Ord A /\ (/) e. A /\ A. b e. A suc b e. A ) <-> ( Ord A /\ A. b e. A suc b e. A /\ A =/= (/) ) )
9 1 8 bitri 
 |-  ( Lim A <-> ( Ord A /\ A. b e. A suc b e. A /\ A =/= (/) ) )