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

Metamath Proof Explorer

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 𝑥 ) = 𝐵 )