Metamath Proof Explorer


Theorem ssorduni

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

Ref Expression
Assertion ssorduni AOnOrdA

Proof

Step Hyp Ref Expression
1 eluni2 xAyAxy
2 ssel AOnyAyOn
3 onelss yOnxyxy
4 2 3 syl6 AOnyAxyxy
5 anc2r yAxyxyyAxyxyyA
6 4 5 syl AOnyAxyxyyA
7 ssuni xyyAxA
8 6 7 syl8 AOnyAxyxA
9 8 rexlimdv AOnyAxyxA
10 1 9 syl5bi AOnxAxA
11 10 ralrimiv AOnxAxA
12 dftr3 TrAxAxA
13 11 12 sylibr AOnTrA
14 onelon yOnxyxOn
15 14 ex yOnxyxOn
16 2 15 syl6 AOnyAxyxOn
17 16 rexlimdv AOnyAxyxOn
18 1 17 syl5bi AOnxAxOn
19 18 ssrdv AOnAOn
20 ordon OrdOn
21 trssord TrAAOnOrdOnOrdA
22 21 3exp TrAAOnOrdOnOrdA
23 20 22 mpii TrAAOnOrdA
24 13 19 23 sylc AOnOrdA