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

Metamath Proof Explorer

Theorem ssorduni

Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of TakeutiZaring p. 40. Lemma 2.7 of Schloeder p. 4. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ssorduni ( 𝐴 ⊆ On → Ord ∪ 𝐴 )

Proof

Step Hyp Ref Expression
1 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
2 ssel ⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On ) )
3 onelss ⊢ ( 𝑦 ∈ On → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) )
4 2 3 syl6 ⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) ) )
5 anc2r ⊢ ( ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦 ) ) → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ) )
6 4 5 syl ⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ) ) )
7 ssuni ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ⊆ ∪ 𝐴 )
8 6 7 syl8 ⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴 ) ) )
9 8 rexlimdv ⊢ ( 𝐴 ⊆ On → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴 ) )
10 1 9 biimtrid ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ⊆ ∪ 𝐴 ) )
11 10 ralrimiv ⊢ ( 𝐴 ⊆ On → ∀ 𝑥 ∈ ∪ 𝐴 𝑥 ⊆ ∪ 𝐴 )
12 dftr3 ⊢ ( Tr ∪ 𝐴 ↔ ∀ 𝑥 ∈ ∪ 𝐴 𝑥 ⊆ ∪ 𝐴 )
13 11 12 sylibr ⊢ ( 𝐴 ⊆ On → Tr ∪ 𝐴 )
14 onelon ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ On )
15 14 ex ⊢ ( 𝑦 ∈ On → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ On ) )
16 2 15 syl6 ⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ On ) ) )
17 16 rexlimdv ⊢ ( 𝐴 ⊆ On → ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ∈ On ) )
18 1 17 biimtrid ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ On ) )
19 18 ssrdv ⊢ ( 𝐴 ⊆ On → ∪ 𝐴 ⊆ On )
20 ordon ⊢ Ord On
21 trssord ⊢ ( ( Tr ∪ 𝐴 ∧ ∪ 𝐴 ⊆ On ∧ Ord On ) → Ord ∪ 𝐴 )
22 21 3exp ⊢ ( Tr ∪ 𝐴 → ( ∪ 𝐴 ⊆ On → ( Ord On → Ord ∪ 𝐴 ) ) )
23 20 22 mpii ⊢ ( Tr ∪ 𝐴 → ( ∪ 𝐴 ⊆ On → Ord ∪ 𝐴 ) )
24 13 19 23 sylc ⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )