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 ) )