Theorem fvrcllb0d

Description: A restriction of the identity relation is a subset of the reflexive closure of a set. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypothesis	fvrcllb0d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	fvrcllb0d	⊢ ( 𝜑 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( r* ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fvrcllb0d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		dfrcl4	⊢ r* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 0 , 1 } ( 𝑟 ↑𝑟 𝑛 ) )
3		prex	⊢ { 0 , 1 } ∈ V
4	3	a1i	⊢ ( 𝜑 → { 0 , 1 } ∈ V )
5		c0ex	⊢ 0 ∈ V
6	5	prid1	⊢ 0 ∈ { 0 , 1 }
7	6	a1i	⊢ ( 𝜑 → 0 ∈ { 0 , 1 } )
8	2 1 4 7	fvmptiunrelexplb0d	⊢ ( 𝜑 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ( r* ‘ 𝑅 ) )