Metamath Proof Explorer

Theorem ordeldifsucon

Description: Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025)

Ref Expression
Assertion ordeldifsucon 
|- ( ( Ord A /\ B e. On ) -> ( C e. ( A \ suc B ) <-> ( C e. A /\ B e. C ) ) )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( C e. ( A \ suc B ) <-> ( C e. A /\ -. C e. suc B ) )
2 simplr 
 |-  ( ( ( Ord A /\ B e. On ) /\ C e. A ) -> B e. On )
3 ordelord 
 |-  ( ( Ord A /\ C e. A ) -> Ord C )
4 3 adantlr 
 |-  ( ( ( Ord A /\ B e. On ) /\ C e. A ) -> Ord C )
5 ordelsuc 
 |-  ( ( B e. On /\ Ord C ) -> ( B e. C <-> suc B C_ C ) )
6 2 4 5 syl2anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ C e. A ) -> ( B e. C <-> suc B C_ C ) )
7 eloni 
 |-  ( B e. On -> Ord B )
8 ordsuci 
 |-  ( Ord B -> Ord suc B )
9 2 7 8 3syl 
 |-  ( ( ( Ord A /\ B e. On ) /\ C e. A ) -> Ord suc B )
10 ordtri1 
 |-  ( ( Ord suc B /\ Ord C ) -> ( suc B C_ C <-> -. C e. suc B ) )
11 9 4 10 syl2anc 
 |-  ( ( ( Ord A /\ B e. On ) /\ C e. A ) -> ( suc B C_ C <-> -. C e. suc B ) )
12 6 11 bitr2d 
 |-  ( ( ( Ord A /\ B e. On ) /\ C e. A ) -> ( -. C e. suc B <-> B e. C ) )
13 12 pm5.32da 
 |-  ( ( Ord A /\ B e. On ) -> ( ( C e. A /\ -. C e. suc B ) <-> ( C e. A /\ B e. C ) ) )
14 1 13 bitrid 
 |-  ( ( Ord A /\ B e. On ) -> ( C e. ( A \ suc B ) <-> ( C e. A /\ B e. C ) ) )