Theorem omabslem

Description: Lemma for omabs . (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Assertion	omabslem	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o ω ) = ω )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		limom	⊢ Lim ω
3	2	jctr	⊢ ( ω ∈ On → ( ω ∈ On ∧ Lim ω ) )
4		omlim	⊢ ( ( 𝐴 ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) → ( 𝐴 ·o ω ) = ∪ 𝑥 ∈ ω ( 𝐴 ·o 𝑥 ) )
5	1 3 4	syl2an	⊢ ( ( 𝐴 ∈ ω ∧ ω ∈ On ) → ( 𝐴 ·o ω ) = ∪ 𝑥 ∈ ω ( 𝐴 ·o 𝑥 ) )
6		ordom	⊢ Ord ω
7		nnmcl	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 ·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	15	3adant3	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o ω ) ⊆ ω )
17		omword2	⊢ ( ( ( ω ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ω ⊆ ( 𝐴 ·o ω ) )
18	17	3impa	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ω ⊆ ( 𝐴 ·o ω ) )
19	1 18	syl3an2	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) → ω ⊆ ( 𝐴 ·o ω ) )
20	16 19	eqssd	⊢ ( ( ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ·o ω ) = ω )