Theorem fvrcllb0da

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

	Ref	Expression
Hypotheses	fvrcllb0da.rel	⊢ ( 𝜑 → Rel 𝑅 )
	fvrcllb0da.r	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	fvrcllb0da	⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( r* ‘ 𝑅 ) )

Proof

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