Theorem wdomref

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

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

Proof

Step	Hyp	Ref	Expression
1		resiexg	$$⊢X\in V\to {\mathrm{I}\upharpoonright }_X\in \mathrm{V}$$
2		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X$$
3		f1ofo	$$⊢\left({\mathrm{I}\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\to \left({\mathrm{I}\upharpoonright }_X\right):X\underset{onto}{⟶}X$$
4	2 3	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_X\right):X\underset{onto}{⟶}X$$
5		fowdom	$$⊢\left({\mathrm{I}\upharpoonright }_X\in \mathrm{V}\wedge \left({\mathrm{I}\upharpoonright }_X\right):X\underset{onto}{⟶}X\right)\to X{\preccurlyeq }^{*}X$$
6	1 4 5	sylancl	$$⊢X\in V\to X{\preccurlyeq }^{*}X$$