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

Metamath Proof Explorer

Theorem wdomref

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

		Ref	Expression
	Assertion	wdomref	$⊢ X \in V \to X ≼^{*} X$

Step	Hyp	Ref	Expression
1		resiexg	$⊢ X \in V \to {I ↾}_{X} \in V$
2		f1oi	$⊢ ({I ↾}_{X}) : X \underset{1-1 onto}{⟶} X$
3		f1ofo	$⊢ ({I ↾}_{X}) : X \underset{1-1 onto}{⟶} X \to ({I ↾}_{X}) : X \underset{onto}{⟶} X$
4	2 3	ax-mp	$⊢ ({I ↾}_{X}) : X \underset{onto}{⟶} X$
5		fowdom	$⊢ ({I ↾}_{X} \in V \land ({I ↾}_{X}) : X \underset{onto}{⟶} X) \to X ≼^{*} X$
6	1 4 5	sylancl	$⊢ X \in V \to X ≼^{*} X$