Metamath Proof Explorer

Theorem ordeldif1o

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

Ref Expression
Assertion ordeldif1o 
|- ( Ord A -> ( B e. ( A \ 1o ) <-> ( B e. A /\ B =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 difeq2i 
 |-  ( A \ 1o ) = ( A \ suc (/) )
3 2 eleq2i 
 |-  ( B e. ( A \ 1o ) <-> B e. ( A \ suc (/) ) )
4 eldif 
 |-  ( B e. ( A \ suc (/) ) <-> ( B e. A /\ -. B e. suc (/) ) )
5 3 4 bitri 
 |-  ( B e. ( A \ 1o ) <-> ( B e. A /\ -. B e. suc (/) ) )
6 0elon 
 |-  (/) e. On
7 ordelord 
 |-  ( ( Ord A /\ B e. A ) -> Ord B )
8 ordelsuc 
 |-  ( ( (/) e. On /\ Ord B ) -> ( (/) e. B <-> suc (/) C_ B ) )
9 6 7 8 sylancr 
 |-  ( ( Ord A /\ B e. A ) -> ( (/) e. B <-> suc (/) C_ B ) )
10 ord0eln0 
 |-  ( Ord B -> ( (/) e. B <-> B =/= (/) ) )
11 7 10 syl 
 |-  ( ( Ord A /\ B e. A ) -> ( (/) e. B <-> B =/= (/) ) )
12 eloni 
 |-  ( (/) e. On -> Ord (/) )
13 ordsuci 
 |-  ( Ord (/) -> Ord suc (/) )
14 6 12 13 mp2b 
 |-  Ord suc (/)
15 ordtri1 
 |-  ( ( Ord suc (/) /\ Ord B ) -> ( suc (/) C_ B <-> -. B e. suc (/) ) )
16 14 7 15 sylancr 
 |-  ( ( Ord A /\ B e. A ) -> ( suc (/) C_ B <-> -. B e. suc (/) ) )
17 9 11 16 3bitr3rd 
 |-  ( ( Ord A /\ B e. A ) -> ( -. B e. suc (/) <-> B =/= (/) ) )
18 17 pm5.32da 
 |-  ( Ord A -> ( ( B e. A /\ -. B e. suc (/) ) <-> ( B e. A /\ B =/= (/) ) ) )
19 5 18 bitrid 
 |-  ( Ord A -> ( B e. ( A \ 1o ) <-> ( B e. A /\ B =/= (/) ) ) )