Theorem r1ord3

Description: Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of BellMachover p. 478. (Contributed by NM, 22-Sep-2003)

	Ref	Expression
Assertion	r1ord3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ 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	3	eleq2i	⊢ ( 𝐵 ∈ dom 𝑅1 ↔ 𝐵 ∈ On )
6		r1ord3g	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )
7	4 5 6	syl2anbr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) )