Theorem fvrtrcllb0da

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

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

Proof

Step	Hyp	Ref	Expression
1		fvrtrcllb0da.rel	⊢ ( 𝜑 → Rel 𝑅 )
2		fvrtrcllb0da.r	⊢ ( 𝜑 → 𝑅 ∈ V )
3		dfrtrcl3	⊢ t* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
4		nn0ex	⊢ ℕ0 ∈ V
5	4	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
6		0nn0	⊢ 0 ∈ ℕ0
7	6	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
8	3 2 5 1 7	fvmptiunrelexplb0da	⊢ ( 𝜑 → ( I ↾ ∪ ∪ 𝑅 ) ⊆ ( t* ‘ 𝑅 ) )