This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐵 ) ) )