Theorem oawordeu

Description: Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of TakeutiZaring p. 59. (Contributed by NM, 11-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		sseq1	|- ( A = if ( A e. On , A , (/) ) -> ( A C_ B <-> if ( A e. On , A , (/) ) C_ B ) )
2		oveq1	|- ( A = if ( A e. On , A , (/) ) -> ( A +o x ) = ( if ( A e. On , A , (/) ) +o x ) )
3	2	eqeq1d	|- ( A = if ( A e. On , A , (/) ) -> ( ( A +o x ) = B <-> ( if ( A e. On , A , (/) ) +o x ) = B ) )
4	3	reubidv	|- ( A = if ( A e. On , A , (/) ) -> ( E! x e. On ( A +o x ) = B <-> E! x e. On ( if ( A e. On , A , (/) ) +o x ) = B ) )
5	1 4	imbi12d	|- ( A = if ( A e. On , A , (/) ) -> ( ( A C_ B -> E! x e. On ( A +o x ) = B ) <-> ( if ( A e. On , A , (/) ) C_ B -> E! x e. On ( if ( A e. On , A , (/) ) +o x ) = B ) ) )
6		sseq2	|- ( B = if ( B e. On , B , (/) ) -> ( if ( A e. On , A , (/) ) C_ B <-> if ( A e. On , A , (/) ) C_ if ( B e. On , B , (/) ) ) )
7		eqeq2	|- ( B = if ( B e. On , B , (/) ) -> ( ( if ( A e. On , A , (/) ) +o x ) = B <-> ( if ( A e. On , A , (/) ) +o x ) = if ( B e. On , B , (/) ) ) )
8	7	reubidv	|- ( B = if ( B e. On , B , (/) ) -> ( E! x e. On ( if ( A e. On , A , (/) ) +o x ) = B <-> E! x e. On ( if ( A e. On , A , (/) ) +o x ) = if ( B e. On , B , (/) ) ) )
9	6 8	imbi12d	|- ( B = if ( B e. On , B , (/) ) -> ( ( if ( A e. On , A , (/) ) C_ B -> E! x e. On ( if ( A e. On , A , (/) ) +o x ) = B ) <-> ( if ( A e. On , A , (/) ) C_ if ( B e. On , B , (/) ) -> E! x e. On ( if ( A e. On , A , (/) ) +o x ) = if ( B e. On , B , (/) ) ) ) )
10		0elon	|- (/) e. On
11	10	elimel	|- if ( A e. On , A , (/) ) e. On
12	10	elimel	|- if ( B e. On , B , (/) ) e. On
13		eqid	|- { y e. On | if ( B e. On , B , (/) ) C_ ( if ( A e. On , A , (/) ) +o y ) } = { y e. On | if ( B e. On , B , (/) ) C_ ( if ( A e. On , A , (/) ) +o y ) }
14	11 12 13	oawordeulem	|- ( if ( A e. On , A , (/) ) C_ if ( B e. On , B , (/) ) -> E! x e. On ( if ( A e. On , A , (/) ) +o x ) = if ( B e. On , B , (/) ) )
15	5 9 14	dedth2h	|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> E! x e. On ( A +o x ) = B ) )
16	15	imp	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> E! x e. On ( A +o x ) = B )