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