Metamath Proof Explorer


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 1 fndmi dom 𝑅1 = On
3 2 eleq2i ( 𝐴 ∈ dom 𝑅1𝐴 ∈ On )
4 2 eleq2i ( 𝐵 ∈ dom 𝑅1𝐵 ∈ On )
5 r1ord3g ( ( 𝐴 ∈ dom 𝑅1𝐵 ∈ dom 𝑅1 ) → ( 𝐴𝐵 → ( 𝑅1𝐴 ) ⊆ ( 𝑅1𝐵 ) ) )
6 3 4 5 syl2anbr ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴𝐵 → ( 𝑅1𝐴 ) ⊆ ( 𝑅1𝐵 ) ) )