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

Metamath Proof Explorer

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