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

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 ∪ E ) ) “ Trans ) )

Proof

Step Hyp Ref Expression
1 dfon3 ⊢ On = ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) )
2 df-ima ⊢ ( ( SSet ∖ ( I ∪ E ) ) “ Trans ) = ran ( ( SSet ∖ ( I ∪ E ) ) ↾ Trans )
3 df-res ⊢ ( ( SSet ∖ ( I ∪ E ) ) ↾ Trans ) = ( ( SSet ∖ ( I ∪ E ) ) ∩ ( Trans × V ) )
4 indif1 ⊢ ( ( SSet ∖ ( I ∪ E ) ) ∩ ( Trans × V ) ) = ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) )
5 3 4 eqtri ⊢ ( ( SSet ∖ ( I ∪ E ) ) ↾ Trans ) = ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) )
6 5 rneqi ⊢ ran ( ( SSet ∖ ( I ∪ E ) ) ↾ Trans ) = ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) )
7 2 6 eqtri ⊢ ( ( SSet ∖ ( I ∪ E ) ) “ Trans ) = ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) )
8 7 difeq2i ⊢ ( V ∖ ( ( SSet ∖ ( I ∪ E ) ) “ Trans ) ) = ( V ∖ ran ( ( SSet ∩ ( Trans × V ) ) ∖ ( I ∪ E ) ) )
9 1 8 eqtr4i ⊢ On = ( V ∖ ( ( SSet ∖ ( I ∪ E ) ) “ Trans ) )