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	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → ( 𝐴 ⊆ 𝐵 ↔ if ( 𝐴 ∈ On , 𝐴 , ∅ ) ⊆ 𝐵 ) )
2		oveq1	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → ( 𝐴 +o 𝑥 ) = ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) )
3	2	eqeq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → ( ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = 𝐵 ) )
4	3	reubidv	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → ( ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ↔ ∃! 𝑥 ∈ On ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = 𝐵 ) )
5	1 4	imbi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ On , 𝐴 , ∅ ) → ( ( 𝐴 ⊆ 𝐵 → ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ) ↔ ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) ⊆ 𝐵 → ∃! 𝑥 ∈ On ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = 𝐵 ) ) )
6		sseq2	⊢ ( 𝐵 = if ( 𝐵 ∈ On , 𝐵 , ∅ ) → ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) ⊆ 𝐵 ↔ if ( 𝐴 ∈ On , 𝐴 , ∅ ) ⊆ if ( 𝐵 ∈ On , 𝐵 , ∅ ) ) )
7		eqeq2	⊢ ( 𝐵 = if ( 𝐵 ∈ On , 𝐵 , ∅ ) → ( ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = 𝐵 ↔ ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = if ( 𝐵 ∈ On , 𝐵 , ∅ ) ) )
8	7	reubidv	⊢ ( 𝐵 = if ( 𝐵 ∈ On , 𝐵 , ∅ ) → ( ∃! 𝑥 ∈ On ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = 𝐵 ↔ ∃! 𝑥 ∈ On ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = if ( 𝐵 ∈ On , 𝐵 , ∅ ) ) )
9	6 8	imbi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ On , 𝐵 , ∅ ) → ( ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) ⊆ 𝐵 → ∃! 𝑥 ∈ On ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = 𝐵 ) ↔ ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) ⊆ if ( 𝐵 ∈ On , 𝐵 , ∅ ) → ∃! 𝑥 ∈ On ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = if ( 𝐵 ∈ On , 𝐵 , ∅ ) ) ) )
10		0elon	⊢ ∅ ∈ On
11	10	elimel	⊢ if ( 𝐴 ∈ On , 𝐴 , ∅ ) ∈ On
12	10	elimel	⊢ if ( 𝐵 ∈ On , 𝐵 , ∅ ) ∈ On
13		eqid	⊢ { 𝑦 ∈ On ∣ if ( 𝐵 ∈ On , 𝐵 , ∅ ) ⊆ ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑦 ) } = { 𝑦 ∈ On ∣ if ( 𝐵 ∈ On , 𝐵 , ∅ ) ⊆ ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑦 ) }
14	11 12 13	oawordeulem	⊢ ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) ⊆ if ( 𝐵 ∈ On , 𝐵 , ∅ ) → ∃! 𝑥 ∈ On ( if ( 𝐴 ∈ On , 𝐴 , ∅ ) +o 𝑥 ) = if ( 𝐵 ∈ On , 𝐵 , ∅ ) )
15	5 9 14	dedth2h	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 ) )
16	15	imp	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( 𝐴 +o 𝑥 ) = 𝐵 )