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