Metamath Proof Explorer


Theorem smoiun

Description: The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011)

Ref Expression
Assertion smoiun SmoBAdomBxABxBA

Proof

Step Hyp Ref Expression
1 eliun yxABxxAyBx
2 smofvon SmoBAdomBBAOn
3 smoel SmoBAdomBxABxBA
4 3 3expia SmoBAdomBxABxBA
5 ontr1 BAOnyBxBxBAyBA
6 5 expcomd BAOnBxBAyBxyBA
7 2 4 6 sylsyld SmoBAdomBxAyBxyBA
8 7 rexlimdv SmoBAdomBxAyBxyBA
9 1 8 syl5bi SmoBAdomByxABxyBA
10 9 ssrdv SmoBAdomBxABxBA