Metamath Proof Explorer


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 𝐴 ) )