Theorem r1ord2

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 22-Sep-2003)

	Ref	Expression
Assertion	r1ord2	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1tr	⊢ Tr ( 𝑅1 ‘ 𝐵 )
2		r1ord	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )
3		trss	⊢ ( Tr ( 𝑅1 ‘ 𝐵 ) → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
4	1 2 3	mpsylsyld	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )