Metamath Proof Explorer


Theorem rankssb

Description: The subset relation is inherited by the rank function. Exercise 1 of TakeutiZaring p. 80. (Contributed by NM, 25-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankssb ( 𝐵 ( 𝑅1 “ On ) → ( 𝐴𝐵 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐵 ( 𝑅1 “ On ) ∧ 𝐴𝐵 ) → 𝐴𝐵 )
2 r1rankidb ( 𝐵 ( 𝑅1 “ On ) → 𝐵 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) )
3 2 adantr ( ( 𝐵 ( 𝑅1 “ On ) ∧ 𝐴𝐵 ) → 𝐵 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) )
4 1 3 sstrd ( ( 𝐵 ( 𝑅1 “ On ) ∧ 𝐴𝐵 ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) )
5 sswf ( ( 𝐵 ( 𝑅1 “ On ) ∧ 𝐴𝐵 ) → 𝐴 ( 𝑅1 “ On ) )
6 rankdmr1 ( rank ‘ 𝐵 ) ∈ dom 𝑅1
7 rankr1bg ( ( 𝐴 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐵 ) ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ↔ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ) )
8 5 6 7 sylancl ( ( 𝐵 ( 𝑅1 “ On ) ∧ 𝐴𝐵 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ↔ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ) )
9 4 8 mpbid ( ( 𝐵 ( 𝑅1 “ On ) ∧ 𝐴𝐵 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) )
10 9 ex ( 𝐵 ( 𝑅1 “ On ) → ( 𝐴𝐵 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) ) )