Theorem oawordexr

Description: Existence theorem for weak ordering of ordinal sum. (Contributed by NM, 12-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		oaword1	|- ( ( A e. On /\ x e. On ) -> A C_ ( A +o x ) )
2		sseq2	|- ( ( A +o x ) = B -> ( A C_ ( A +o x ) <-> A C_ B ) )
3	1 2	syl5ibcom	|- ( ( A e. On /\ x e. On ) -> ( ( A +o x ) = B -> A C_ B ) )
4	3	rexlimdva	|- ( A e. On -> ( E. x e. On ( A +o x ) = B -> A C_ B ) )
5	4	imp	|- ( ( A e. On /\ E. x e. On ( A +o x ) = B ) -> A C_ B )