Theorem r1ord

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 8-Sep-2003) (Revised by Mario Carneiro, 16-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		r1fnon	⊢ 𝑅1 Fn On
2		fndm	⊢ ( 𝑅1 Fn On → dom 𝑅1 = On )
3	1 2	ax-mp	⊢ dom 𝑅1 = On
4	3	eleq2i	⊢ ( 𝐵 ∈ dom 𝑅1 ↔ 𝐵 ∈ On )
5		r1ordg	⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )
6	4 5	sylbir	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )