Theorem r1sssuc

Description: The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011)

	Ref	Expression
Assertion	r1sssuc	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ suc 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		r1tr	⊢ Tr ( 𝑅1 ‘ 𝐴 )
2		dftr4	⊢ ( Tr ( 𝑅1 ‘ 𝐴 ) ↔ ( 𝑅1 ‘ 𝐴 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝐴 ) )
3	1 2	mpbi	⊢ ( 𝑅1 ‘ 𝐴 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝐴 )
4		r1suc	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
5	3 4	sseqtrrid	⊢ ( 𝐴 ∈ On → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ suc 𝐴 ) )