Theorem fvtrcllb1d

Description: A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypothesis	fvtrcllb1d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	fvtrcllb1d	⊢ ( 𝜑 → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fvtrcllb1d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		dftrcl3	⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
3		nnex	⊢ ℕ ∈ V
4	3	a1i	⊢ ( 𝜑 → ℕ ∈ V )
5		1nn	⊢ 1 ∈ ℕ
6	5	a1i	⊢ ( 𝜑 → 1 ∈ ℕ )
7	2 1 4 6	fvmptiunrelexplb1d	⊢ ( 𝜑 → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )