Step |
Hyp |
Ref |
Expression |
1 |
|
r1funlim |
⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 ) |
2 |
1
|
simpri |
⊢ Lim dom 𝑅1 |
3 |
|
limord |
⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 ) |
4 |
|
ordsson |
⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On ) |
5 |
2 3 4
|
mp2b |
⊢ dom 𝑅1 ⊆ On |
6 |
5
|
sseli |
⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ∈ On ) |
7 |
5
|
sseli |
⊢ ( 𝐵 ∈ dom 𝑅1 → 𝐵 ∈ On ) |
8 |
|
onsseleq |
⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) ) |
9 |
6 7 8
|
syl2an |
⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) ) ) |
10 |
|
r1tr |
⊢ Tr ( 𝑅1 ‘ 𝐵 ) |
11 |
|
r1ordg |
⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) ) |
13 |
|
trss |
⊢ ( Tr ( 𝑅1 ‘ 𝐵 ) → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) |
14 |
10 12 13
|
mpsylsyld |
⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) |
15 |
|
fveq2 |
⊢ ( 𝐴 = 𝐵 → ( 𝑅1 ‘ 𝐴 ) = ( 𝑅1 ‘ 𝐵 ) ) |
16 |
|
eqimss |
⊢ ( ( 𝑅1 ‘ 𝐴 ) = ( 𝑅1 ‘ 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) |
17 |
15 16
|
syl |
⊢ ( 𝐴 = 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) |
18 |
17
|
a1i |
⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 = 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) |
19 |
14 18
|
jaod |
⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) |
20 |
9 19
|
sylbid |
⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐵 ) ) ) |