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