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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluni2 | |
|
2 | ssel | |
|
3 | onelss | |
|
4 | 2 3 | syl6 | |
5 | anc2r | |
|
6 | 4 5 | syl | |
7 | ssuni | |
|
8 | 6 7 | syl8 | |
9 | 8 | rexlimdv | |
10 | 1 9 | syl5bi | |
11 | 10 | ralrimiv | |
12 | dftr3 | |
|
13 | 11 12 | sylibr | |
14 | onelon | |
|
15 | 14 | ex | |
16 | 2 15 | syl6 | |
17 | 16 | rexlimdv | |
18 | 1 17 | syl5bi | |
19 | 18 | ssrdv | |
20 | ordon | |
|
21 | trssord | |
|
22 | 21 | 3exp | |
23 | 20 22 | mpii | |
24 | 13 19 23 | sylc | |