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