This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oawordex

Description: Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of TakeutiZaring p. 59 and its converse. See oawordeu for uniqueness. (Contributed by NM, 12-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oawordeu 
 |-  ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> E! x e. On ( A +o x ) = B )
2 1 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B -> E! x e. On ( A +o x ) = B ) )
3 reurex 
 |-  ( E! x e. On ( A +o x ) = B -> E. x e. On ( A +o x ) = B )
4 2 3 syl6 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B -> E. x e. On ( A +o x ) = B ) )
5 oawordexr 
 |-  ( ( A e. On /\ E. x e. On ( A +o x ) = B ) -> A C_ B )
6 5 ex 
 |-  ( A e. On -> ( E. x e. On ( A +o x ) = B -> A C_ B ) )
7 6 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( E. x e. On ( A +o x ) = B -> A C_ B ) )
8 4 7 impbid 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> E. x e. On ( A +o x ) = B ) )