This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmrnssfld

Description: The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008)

Ref Expression
Assertion dmrnssfld 
|- ( dom A u. ran A ) C_ U. U. A

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 eldm2 
 |-  ( x e. dom A <-> E. y <. x , y >. e. A )
3 1 prid1 
 |-  x e. { x , y }
4 vex 
 |-  y e. _V
5 1 4 uniop 
 |-  U. <. x , y >. = { x , y }
6 1 4 uniopel 
 |-  ( <. x , y >. e. A -> U. <. x , y >. e. U. A )
7 5 6 eqeltrrid 
 |-  ( <. x , y >. e. A -> { x , y } e. U. A )
8 elssuni 
 |-  ( { x , y } e. U. A -> { x , y } C_ U. U. A )
9 7 8 syl 
 |-  ( <. x , y >. e. A -> { x , y } C_ U. U. A )
10 9 sseld 
 |-  ( <. x , y >. e. A -> ( x e. { x , y } -> x e. U. U. A ) )
11 3 10 mpi 
 |-  ( <. x , y >. e. A -> x e. U. U. A )
12 11 exlimiv 
 |-  ( E. y <. x , y >. e. A -> x e. U. U. A )
13 2 12 sylbi 
 |-  ( x e. dom A -> x e. U. U. A )
14 13 ssriv 
 |-  dom A C_ U. U. A
15 4 elrn2 
 |-  ( y e. ran A <-> E. x <. x , y >. e. A )
16 4 prid2 
 |-  y e. { x , y }
17 9 sseld 
 |-  ( <. x , y >. e. A -> ( y e. { x , y } -> y e. U. U. A ) )
18 16 17 mpi 
 |-  ( <. x , y >. e. A -> y e. U. U. A )
19 18 exlimiv 
 |-  ( E. x <. x , y >. e. A -> y e. U. U. A )
20 15 19 sylbi 
 |-  ( y e. ran A -> y e. U. U. A )
21 20 ssriv 
 |-  ran A C_ U. U. A
22 14 21 unssi 
 |-  ( dom A u. ran A ) C_ U. U. A