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 
|- ( ( Smo B /\ A e. dom B ) -> U_ x e. A ( B ` x ) C_ ( B ` A ) )

Proof

Step Hyp Ref Expression
1 eliun 
 |-  ( y e. U_ x e. A ( B ` x ) <-> E. x e. A y e. ( B ` x ) )
2 smofvon 
 |-  ( ( Smo B /\ A e. dom B ) -> ( B ` A ) e. On )
3 smoel 
 |-  ( ( Smo B /\ A e. dom B /\ x e. A ) -> ( B ` x ) e. ( B ` A ) )
4 3 3expia 
 |-  ( ( Smo B /\ A e. dom B ) -> ( x e. A -> ( B ` x ) e. ( B ` A ) ) )
5 ontr1 
 |-  ( ( B ` A ) e. On -> ( ( y e. ( B ` x ) /\ ( B ` x ) e. ( B ` A ) ) -> y e. ( B ` A ) ) )
6 5 expcomd 
 |-  ( ( B ` A ) e. On -> ( ( B ` x ) e. ( B ` A ) -> ( y e. ( B ` x ) -> y e. ( B ` A ) ) ) )
7 2 4 6 sylsyld 
 |-  ( ( Smo B /\ A e. dom B ) -> ( x e. A -> ( y e. ( B ` x ) -> y e. ( B ` A ) ) ) )
8 7 rexlimdv 
 |-  ( ( Smo B /\ A e. dom B ) -> ( E. x e. A y e. ( B ` x ) -> y e. ( B ` A ) ) )
9 1 8 biimtrid 
 |-  ( ( Smo B /\ A e. dom B ) -> ( y e. U_ x e. A ( B ` x ) -> y e. ( B ` A ) ) )
10 9 ssrdv 
 |-  ( ( Smo B /\ A e. dom B ) -> U_ x e. A ( B ` x ) C_ ( B ` A ) )