Metamath Proof Explorer

Theorem oawordex2

Description: If C is between A (inclusive) and ( A +o B ) (exclusive), there is an ordinal which equals C when summed to A . This is a slightly different statement than oawordex or oawordeu . (Contributed by RP, 7-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> A C_ C )
2 simpll 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> A e. On )
3 oacl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
4 simpr 
 |-  ( ( A C_ C /\ C e. ( A +o B ) ) -> C e. ( A +o B ) )
5 onelon 
 |-  ( ( ( A +o B ) e. On /\ C e. ( A +o B ) ) -> C e. On )
6 3 4 5 syl2an 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> C e. On )
7 oawordex 
 |-  ( ( A e. On /\ C e. On ) -> ( A C_ C <-> E. x e. On ( A +o x ) = C ) )
8 2 6 7 syl2anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> ( A C_ C <-> E. x e. On ( A +o x ) = C ) )
9 1 8 mpbid 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> E. x e. On ( A +o x ) = C )
10 simprr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> ( A +o x ) = C )
11 simprr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> C e. ( A +o B ) )
12 11 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> C e. ( A +o B ) )
13 10 12 eqeltrd 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> ( A +o x ) e. ( A +o B ) )
14 simprl 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> x e. On )
15 simpllr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> B e. On )
16 2 adantr 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> A e. On )
17 oaord 
 |-  ( ( x e. On /\ B e. On /\ A e. On ) -> ( x e. B <-> ( A +o x ) e. ( A +o B ) ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> ( x e. B <-> ( A +o x ) e. ( A +o B ) ) )
19 13 18 mpbird 
 |-  ( ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) /\ ( x e. On /\ ( A +o x ) = C ) ) -> x e. B )
20 9 19 10 reximssdv 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> E. x e. B ( A +o x ) = C )