Theorem wdomref

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

	Ref	Expression
Assertion	wdomref	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		resiexg	⊢ ( 𝑋 ∈ 𝑉 → ( I ↾ 𝑋 ) ∈ V )
2		f1oi	⊢ ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋
3		f1ofo	⊢ ( ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋 → ( I ↾ 𝑋 ) : 𝑋 –onto→ 𝑋 )
4	2 3	ax-mp	⊢ ( I ↾ 𝑋 ) : 𝑋 –onto→ 𝑋
5		fowdom	⊢ ( ( ( I ↾ 𝑋 ) ∈ V ∧ ( I ↾ 𝑋 ) : 𝑋 –onto→ 𝑋 ) → 𝑋 ≼* 𝑋 )
6	1 4 5	sylancl	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋 )