Metamath Proof Explorer

Theorem riotassuni

Description: The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion riotassuni 
|- ( iota_ x e. A ph ) C_ ( ~P U. A u. U. A )

Proof

Step Hyp Ref Expression
1 riotauni 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) = U. { x e. A | ph } )
2 ssrab2 
 |-  { x e. A | ph } C_ A
3 2 unissi 
 |-  U. { x e. A | ph } C_ U. A
4 ssun2 
 |-  U. A C_ ( ~P U. A u. U. A )
5 3 4 sstri 
 |-  U. { x e. A | ph } C_ ( ~P U. A u. U. A )
6 1 5 eqsstrdi 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) C_ ( ~P U. A u. U. A ) )
7 riotaund 
 |-  ( -. E! x e. A ph -> ( iota_ x e. A ph ) = (/) )
8 0ss 
 |-  (/) C_ ( ~P U. A u. U. A )
9 7 8 eqsstrdi 
 |-  ( -. E! x e. A ph -> ( iota_ x e. A ph ) C_ ( ~P U. A u. U. A ) )
10 6 9 pm2.61i 
 |-  ( iota_ x e. A ph ) C_ ( ~P U. A u. U. A )