Metamath Proof Explorer


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 1 fndmi dom 𝑅1 = On
3 2 eleq2i ( 𝐵 ∈ dom 𝑅1𝐵 ∈ On )
4 r1ordg ( 𝐵 ∈ dom 𝑅1 → ( 𝐴𝐵 → ( 𝑅1𝐴 ) ∈ ( 𝑅1𝐵 ) ) )
5 3 4 sylbir ( 𝐵 ∈ On → ( 𝐴𝐵 → ( 𝑅1𝐴 ) ∈ ( 𝑅1𝐵 ) ) )