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 ) )