Metamath Proof Explorer


Theorem oaabslem

Description: Lemma for oaabs . (Contributed by NM, 9-Dec-2004)

Ref Expression
Assertion oaabslem ( ( ω ∈ On ∧ 𝐴 ∈ ω ) → ( 𝐴 +o ω ) = ω )

Proof

Step Hyp Ref Expression
1 nnon ( 𝐴 ∈ ω → 𝐴 ∈ On )
2 limom Lim ω
3 2 jctr ( ω ∈ On → ( ω ∈ On ∧ Lim ω ) )
4 oalim ( ( 𝐴 ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) → ( 𝐴 +o ω ) = 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) )
5 1 3 4 syl2an ( ( 𝐴 ∈ ω ∧ ω ∈ On ) → ( 𝐴 +o ω ) = 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) )
6 ordom Ord ω
7 nnacl ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) ∈ ω )
8 ordelss ( ( Ord ω ∧ ( 𝐴 +o 𝑥 ) ∈ ω ) → ( 𝐴 +o 𝑥 ) ⊆ ω )
9 6 7 8 sylancr ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 +o 𝑥 ) ⊆ ω )
10 9 ralrimiva ( 𝐴 ∈ ω → ∀ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) ⊆ ω )
11 iunss ( 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) ⊆ ω ↔ ∀ 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) ⊆ ω )
12 10 11 sylibr ( 𝐴 ∈ ω → 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) ⊆ ω )
13 12 adantr ( ( 𝐴 ∈ ω ∧ ω ∈ On ) → 𝑥 ∈ ω ( 𝐴 +o 𝑥 ) ⊆ ω )
14 5 13 eqsstrd ( ( 𝐴 ∈ ω ∧ ω ∈ On ) → ( 𝐴 +o ω ) ⊆ ω )
15 14 ancoms ( ( ω ∈ On ∧ 𝐴 ∈ ω ) → ( 𝐴 +o ω ) ⊆ ω )
16 oaword2 ( ( ω ∈ On ∧ 𝐴 ∈ On ) → ω ⊆ ( 𝐴 +o ω ) )
17 1 16 sylan2 ( ( ω ∈ On ∧ 𝐴 ∈ ω ) → ω ⊆ ( 𝐴 +o ω ) )
18 15 17 eqssd ( ( ω ∈ On ∧ 𝐴 ∈ ω ) → ( 𝐴 +o ω ) = ω )