Metamath Proof Explorer

Theorem dfon4

Description: Another quantifier-free definition of On . (Contributed by Scott Fenton, 4-May-2014)

Ref Expression
Assertion dfon4 
|- On = ( _V \ ( ( SSet \ ( _I u. _E ) ) " Trans ) )

Proof

Step Hyp Ref Expression
1 dfon3 
 |-  On = ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )
2 df-ima 
 |-  ( ( SSet \ ( _I u. _E ) ) " Trans ) = ran ( ( SSet \ ( _I u. _E ) ) |` Trans )
3 df-res 
 |-  ( ( SSet \ ( _I u. _E ) ) |` Trans ) = ( ( SSet \ ( _I u. _E ) ) i^i ( Trans X. _V ) )
4 indif1 
 |-  ( ( SSet \ ( _I u. _E ) ) i^i ( Trans X. _V ) ) = ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) )
5 3 4 eqtri 
 |-  ( ( SSet \ ( _I u. _E ) ) |` Trans ) = ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) )
6 5 rneqi 
 |-  ran ( ( SSet \ ( _I u. _E ) ) |` Trans ) = ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) )
7 2 6 eqtri 
 |-  ( ( SSet \ ( _I u. _E ) ) " Trans ) = ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) )
8 7 difeq2i 
 |-  ( _V \ ( ( SSet \ ( _I u. _E ) ) " Trans ) ) = ( _V \ ran ( ( SSet i^i ( Trans X. _V ) ) \ ( _I u. _E ) ) )
9 1 8 eqtr4i 
 |-  On = ( _V \ ( ( SSet \ ( _I u. _E ) ) " Trans ) )