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

Metamath Proof Explorer

Theorem oaabs

Description: Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of TakeutiZaring p. 59. (Contributed by NM, 9-Dec-2004) (Proof shortened by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion oaabs ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ( 𝐴 +o 𝐵 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 ssexg ⊢ ( ( ω ⊆ 𝐵 ∧ 𝐵 ∈ On ) → ω ∈ V )
2 1 ex ⊢ ( ω ⊆ 𝐵 → ( 𝐵 ∈ On → ω ∈ V ) )
3 omelon2 ⊢ ( ω ∈ V → ω ∈ On )
4 2 3 syl6com ⊢ ( 𝐵 ∈ On → ( ω ⊆ 𝐵 → ω ∈ On ) )
5 4 imp ⊢ ( ( 𝐵 ∈ On ∧ ω ⊆ 𝐵 ) → ω ∈ On )
6 5 adantll ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ω ∈ On )
7 simplr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → 𝐵 ∈ On )
8 6 7 jca ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ( ω ∈ On ∧ 𝐵 ∈ On ) )
9 oawordeu ⊢ ( ( ( ω ∈ On ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ω +o 𝑥 ) = 𝐵 )
10 8 9 sylancom ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ∃! 𝑥 ∈ On ( ω +o 𝑥 ) = 𝐵 )
11 reurex ⊢ ( ∃! 𝑥 ∈ On ( ω +o 𝑥 ) = 𝐵 → ∃ 𝑥 ∈ On ( ω +o 𝑥 ) = 𝐵 )
12 10 11 syl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ∃ 𝑥 ∈ On ( ω +o 𝑥 ) = 𝐵 )
13 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
14 13 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝐴 ∈ On )
15 6 adantr ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ω ∈ On )
16 simpr ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → 𝑥 ∈ On )
17 oaass ⊢ ( ( 𝐴 ∈ On ∧ ω ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ω ) +o 𝑥 ) = ( 𝐴 +o ( ω +o 𝑥 ) ) )
18 14 15 16 17 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ω ) +o 𝑥 ) = ( 𝐴 +o ( ω +o 𝑥 ) ) )
19 simpll ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → 𝐴 ∈ ω )
20 oaabslem ⊢ ( ( ω ∈ On ∧ 𝐴 ∈ ω ) → ( 𝐴 +o ω ) = ω )
21 6 19 20 syl2anc ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ( 𝐴 +o ω ) = ω )
22 21 adantr ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ω ) = ω )
23 22 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( 𝐴 +o ω ) +o 𝑥 ) = ( ω +o 𝑥 ) )
24 18 23 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( 𝐴 +o ( ω +o 𝑥 ) ) = ( ω +o 𝑥 ) )
25 oveq2 ⊢ ( ( ω +o 𝑥 ) = 𝐵 → ( 𝐴 +o ( ω +o 𝑥 ) ) = ( 𝐴 +o 𝐵 ) )
26 id ⊢ ( ( ω +o 𝑥 ) = 𝐵 → ( ω +o 𝑥 ) = 𝐵 )
27 25 26 eqeq12d ⊢ ( ( ω +o 𝑥 ) = 𝐵 → ( ( 𝐴 +o ( ω +o 𝑥 ) ) = ( ω +o 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) = 𝐵 ) )
28 24 27 syl5ibcom ⊢ ( ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) ∧ 𝑥 ∈ On ) → ( ( ω +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) )
29 28 rexlimdva ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ( ∃ 𝑥 ∈ On ( ω +o 𝑥 ) = 𝐵 → ( 𝐴 +o 𝐵 ) = 𝐵 ) )
30 12 29 mpd ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ On ) ∧ ω ⊆ 𝐵 ) → ( 𝐴 +o 𝐵 ) = 𝐵 )