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

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 ω ) = ω )