Metamath Proof Explorer

Theorem dflim6

Description: A limit ordinal is a non-zero ordinal which is not a succesor ordinal. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 ioran 
 |-  ( -. ( A = (/) \/ E. b e. On A = suc b ) <-> ( -. A = (/) /\ -. E. b e. On A = suc b ) )
2 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
3 2 anbi1i 
 |-  ( ( A =/= (/) /\ -. E. b e. On A = suc b ) <-> ( -. A = (/) /\ -. E. b e. On A = suc b ) )
4 1 3 bitr4i 
 |-  ( -. ( A = (/) \/ E. b e. On A = suc b ) <-> ( A =/= (/) /\ -. E. b e. On A = suc b ) )
5 4 anbi2i 
 |-  ( ( Ord A /\ -. ( A = (/) \/ E. b e. On A = suc b ) ) <-> ( Ord A /\ ( A =/= (/) /\ -. E. b e. On A = suc b ) ) )
6 dflim3 
 |-  ( Lim A <-> ( Ord A /\ -. ( A = (/) \/ E. b e. On A = suc b ) ) )
7 3anass 
 |-  ( ( Ord A /\ A =/= (/) /\ -. E. b e. On A = suc b ) <-> ( Ord A /\ ( A =/= (/) /\ -. E. b e. On A = suc b ) ) )
8 5 6 7 3bitr4i 
 |-  ( Lim A <-> ( Ord A /\ A =/= (/) /\ -. E. b e. On A = suc b ) )