Description: The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | smoiun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliun | |
|
2 | smofvon | |
|
3 | smoel | |
|
4 | 3 | 3expia | |
5 | ontr1 | |
|
6 | 5 | expcomd | |
7 | 2 4 6 | sylsyld | |
8 | 7 | rexlimdv | |
9 | 1 8 | syl5bi | |
10 | 9 | ssrdv | |