Step |
Hyp |
Ref |
Expression |
1 |
|
tposfun |
⊢ ( Fun 𝐹 → Fun tpos 𝐹 ) |
2 |
1
|
a1i |
⊢ ( Rel 𝐴 → ( Fun 𝐹 → Fun tpos 𝐹 ) ) |
3 |
|
dmtpos |
⊢ ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 ) |
4 |
3
|
a1i |
⊢ ( dom 𝐹 = 𝐴 → ( Rel dom 𝐹 → dom tpos 𝐹 = ◡ dom 𝐹 ) ) |
5 |
|
releq |
⊢ ( dom 𝐹 = 𝐴 → ( Rel dom 𝐹 ↔ Rel 𝐴 ) ) |
6 |
|
cnveq |
⊢ ( dom 𝐹 = 𝐴 → ◡ dom 𝐹 = ◡ 𝐴 ) |
7 |
6
|
eqeq2d |
⊢ ( dom 𝐹 = 𝐴 → ( dom tpos 𝐹 = ◡ dom 𝐹 ↔ dom tpos 𝐹 = ◡ 𝐴 ) ) |
8 |
4 5 7
|
3imtr3d |
⊢ ( dom 𝐹 = 𝐴 → ( Rel 𝐴 → dom tpos 𝐹 = ◡ 𝐴 ) ) |
9 |
8
|
com12 |
⊢ ( Rel 𝐴 → ( dom 𝐹 = 𝐴 → dom tpos 𝐹 = ◡ 𝐴 ) ) |
10 |
2 9
|
anim12d |
⊢ ( Rel 𝐴 → ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) → ( Fun tpos 𝐹 ∧ dom tpos 𝐹 = ◡ 𝐴 ) ) ) |
11 |
|
df-fn |
⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ) |
12 |
|
df-fn |
⊢ ( tpos 𝐹 Fn ◡ 𝐴 ↔ ( Fun tpos 𝐹 ∧ dom tpos 𝐹 = ◡ 𝐴 ) ) |
13 |
10 11 12
|
3imtr4g |
⊢ ( Rel 𝐴 → ( 𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡ 𝐴 ) ) |