Metamath Proof Explorer

Theorem oasubex

Description: While subtraction can't be a binary operation on ordinals, for any pair of ordinals there exists an ordinal that can be added to the lessor (or equal) one which will sum to the greater. Theorem 2.19 of Schloeder p. 6. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion oasubex 
|- ( ( A e. On /\ B e. On /\ B C_ A ) -> E. c e. On ( c C_ A /\ ( B +o c ) = A ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. On /\ B e. On /\ B C_ A ) -> B e. On )
2 simp1 
 |-  ( ( A e. On /\ B e. On /\ B C_ A ) -> A e. On )
3 simp3 
 |-  ( ( A e. On /\ B e. On /\ B C_ A ) -> B C_ A )
4 oawordex 
 |-  ( ( B e. On /\ A e. On ) -> ( B C_ A <-> E. c e. On ( B +o c ) = A ) )
5 4 biimpa 
 |-  ( ( ( B e. On /\ A e. On ) /\ B C_ A ) -> E. c e. On ( B +o c ) = A )
6 1 2 3 5 syl21anc 
 |-  ( ( A e. On /\ B e. On /\ B C_ A ) -> E. c e. On ( B +o c ) = A )
7 simpr 
 |-  ( ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) /\ ( B +o c ) = A ) -> ( B +o c ) = A )
8 simpl1 
 |-  ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) -> A e. On )
9 simpl2 
 |-  ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) -> B e. On )
10 oaword2 
 |-  ( ( A e. On /\ B e. On ) -> A C_ ( B +o A ) )
11 8 9 10 syl2anc 
 |-  ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) -> A C_ ( B +o A ) )
12 11 adantr 
 |-  ( ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) /\ ( B +o c ) = A ) -> A C_ ( B +o A ) )
13 7 12 eqsstrd 
 |-  ( ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) /\ ( B +o c ) = A ) -> ( B +o c ) C_ ( B +o A ) )
14 simpr 
 |-  ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) -> c e. On )
15 oaword 
 |-  ( ( c e. On /\ A e. On /\ B e. On ) -> ( c C_ A <-> ( B +o c ) C_ ( B +o A ) ) )
16 14 8 9 15 syl3anc 
 |-  ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) -> ( c C_ A <-> ( B +o c ) C_ ( B +o A ) ) )
17 16 adantr 
 |-  ( ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) /\ ( B +o c ) = A ) -> ( c C_ A <-> ( B +o c ) C_ ( B +o A ) ) )
18 13 17 mpbird 
 |-  ( ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) /\ ( B +o c ) = A ) -> c C_ A )
19 18 ex 
 |-  ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) -> ( ( B +o c ) = A -> c C_ A ) )
20 19 ancrd 
 |-  ( ( ( A e. On /\ B e. On /\ B C_ A ) /\ c e. On ) -> ( ( B +o c ) = A -> ( c C_ A /\ ( B +o c ) = A ) ) )
21 20 reximdva 
 |-  ( ( A e. On /\ B e. On /\ B C_ A ) -> ( E. c e. On ( B +o c ) = A -> E. c e. On ( c C_ A /\ ( B +o c ) = A ) ) )
22 6 21 mpd 
 |-  ( ( A e. On /\ B e. On /\ B C_ A ) -> E. c e. On ( c C_ A /\ ( B +o c ) = A ) )