| Step |
Hyp |
Ref |
Expression |
| 1 |
|
bj-cnvresrn |
⊢ ( ◡ 𝐴 ↾ ran 𝐴 ) = ◡ 𝐴 |
| 2 |
|
simpr |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → ran 𝐴 ⊆ dom 𝐵 ) |
| 3 |
|
ssres2 |
⊢ ( ran 𝐴 ⊆ dom 𝐵 → ( ◡ 𝐴 ↾ ran 𝐴 ) ⊆ ( ◡ 𝐴 ↾ dom 𝐵 ) ) |
| 4 |
2 3
|
syl |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → ( ◡ 𝐴 ↾ ran 𝐴 ) ⊆ ( ◡ 𝐴 ↾ dom 𝐵 ) ) |
| 5 |
|
simpl |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → ( 𝐵 ∘ 𝐴 ) ⊆ I ) |
| 6 |
|
cossidres2 |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ 𝐴 ↾ dom 𝐵 ) ⊆ 𝐵 ) |
| 7 |
5 6
|
syl |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → ( ◡ 𝐴 ↾ dom 𝐵 ) ⊆ 𝐵 ) |
| 8 |
4 7
|
sstrd |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → ( ◡ 𝐴 ↾ ran 𝐴 ) ⊆ 𝐵 ) |
| 9 |
1 8
|
eqsstrrid |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → ◡ 𝐴 ⊆ 𝐵 ) |
| 10 |
|
relres |
⊢ Rel ( 𝐵 ↾ ran 𝐴 ) |
| 11 |
10
|
a1i |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → Rel ( 𝐵 ↾ ran 𝐴 ) ) |
| 12 |
|
resss |
⊢ ( 𝐵 ↾ ran 𝐴 ) ⊆ 𝐵 |
| 13 |
12
|
a1i |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ↾ ran 𝐴 ) ⊆ 𝐵 ) |
| 14 |
|
cossidres1 |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ 𝐴 ) |
| 15 |
|
cnvss |
⊢ ( ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ 𝐴 → ◡ ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ ◡ 𝐴 ) |
| 16 |
14 15
|
syl |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ◡ ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ ◡ 𝐴 ) |
| 17 |
|
cnvcnvss |
⊢ ◡ ◡ 𝐴 ⊆ 𝐴 |
| 18 |
16 17
|
sstrdi |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ◡ ( 𝐵 ↾ ran 𝐴 ) ⊆ 𝐴 ) |
| 19 |
13 18
|
coss12d |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ( 𝐵 ↾ ran 𝐴 ) ) ⊆ ( 𝐵 ∘ 𝐴 ) ) |
| 20 |
|
id |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ∘ 𝐴 ) ⊆ I ) |
| 21 |
19 20
|
sstrd |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ( 𝐵 ↾ ran 𝐴 ) ) ⊆ I ) |
| 22 |
|
df-fun |
⊢ ( Fun ( 𝐵 ↾ ran 𝐴 ) ↔ ( Rel ( 𝐵 ↾ ran 𝐴 ) ∧ ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ( 𝐵 ↾ ran 𝐴 ) ) ⊆ I ) ) |
| 23 |
11 21 22
|
sylanbrc |
⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → Fun ( 𝐵 ↾ ran 𝐴 ) ) |
| 24 |
5 23
|
syl |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → Fun ( 𝐵 ↾ ran 𝐴 ) ) |
| 25 |
9 24
|
jca |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) → ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) ) |
| 26 |
|
coresrn |
⊢ ( ( 𝐵 ↾ ran 𝐴 ) ∘ 𝐴 ) = ( 𝐵 ∘ 𝐴 ) |
| 27 |
|
cocnvcnv2 |
⊢ ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ◡ 𝐴 ) = ( ( 𝐵 ↾ ran 𝐴 ) ∘ 𝐴 ) |
| 28 |
|
simpl |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ◡ 𝐴 ⊆ 𝐵 ) |
| 29 |
|
ssres |
⊢ ( ◡ 𝐴 ⊆ 𝐵 → ( ◡ 𝐴 ↾ ran 𝐴 ) ⊆ ( 𝐵 ↾ ran 𝐴 ) ) |
| 30 |
28 29
|
syl |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ( ◡ 𝐴 ↾ ran 𝐴 ) ⊆ ( 𝐵 ↾ ran 𝐴 ) ) |
| 31 |
1 30
|
eqsstrrid |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ◡ 𝐴 ⊆ ( 𝐵 ↾ ran 𝐴 ) ) |
| 32 |
|
cnvss |
⊢ ( ◡ 𝐴 ⊆ ( 𝐵 ↾ ran 𝐴 ) → ◡ ◡ 𝐴 ⊆ ◡ ( 𝐵 ↾ ran 𝐴 ) ) |
| 33 |
31 32
|
syl |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ◡ ◡ 𝐴 ⊆ ◡ ( 𝐵 ↾ ran 𝐴 ) ) |
| 34 |
|
coss2 |
⊢ ( ◡ ◡ 𝐴 ⊆ ◡ ( 𝐵 ↾ ran 𝐴 ) → ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ◡ 𝐴 ) ⊆ ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ( 𝐵 ↾ ran 𝐴 ) ) ) |
| 35 |
33 34
|
syl |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ◡ 𝐴 ) ⊆ ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ( 𝐵 ↾ ran 𝐴 ) ) ) |
| 36 |
|
simpr |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → Fun ( 𝐵 ↾ ran 𝐴 ) ) |
| 37 |
22
|
simprbi |
⊢ ( Fun ( 𝐵 ↾ ran 𝐴 ) → ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ( 𝐵 ↾ ran 𝐴 ) ) ⊆ I ) |
| 38 |
36 37
|
syl |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ( 𝐵 ↾ ran 𝐴 ) ) ⊆ I ) |
| 39 |
35 38
|
sstrd |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ( ( 𝐵 ↾ ran 𝐴 ) ∘ ◡ ◡ 𝐴 ) ⊆ I ) |
| 40 |
27 39
|
eqsstrrid |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ( ( 𝐵 ↾ ran 𝐴 ) ∘ 𝐴 ) ⊆ I ) |
| 41 |
26 40
|
eqsstrrid |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ( 𝐵 ∘ 𝐴 ) ⊆ I ) |
| 42 |
|
df-rn |
⊢ ran 𝐴 = dom ◡ 𝐴 |
| 43 |
|
dmss |
⊢ ( ◡ 𝐴 ⊆ 𝐵 → dom ◡ 𝐴 ⊆ dom 𝐵 ) |
| 44 |
28 43
|
syl |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → dom ◡ 𝐴 ⊆ dom 𝐵 ) |
| 45 |
42 44
|
eqsstrid |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ran 𝐴 ⊆ dom 𝐵 ) |
| 46 |
41 45
|
jca |
⊢ ( ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) → ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) ) |
| 47 |
25 46
|
impbii |
⊢ ( ( ( 𝐵 ∘ 𝐴 ) ⊆ I ∧ ran 𝐴 ⊆ dom 𝐵 ) ↔ ( ◡ 𝐴 ⊆ 𝐵 ∧ Fun ( 𝐵 ↾ ran 𝐴 ) ) ) |