Theorem wdomref

Description: Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	wdomref	|- ( X e. V -> X ~<_* X )

Proof

Step	Hyp	Ref	Expression
1		resiexg	|- ( X e. V -> ( _I |` X ) e. _V )
2		f1oi	|- ( _I |` X ) : X -1-1-onto-> X
3		f1ofo	|- ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X -onto-> X )
4	2 3	ax-mp	|- ( _I |` X ) : X -onto-> X
5		fowdom	|- ( ( ( _I |` X ) e. _V /\ ( _I |` X ) : X -onto-> X ) -> X ~<_* X )
6	1 4 5	sylancl	|- ( X e. V -> X ~<_* X )