Step | Hyp | Ref
| Expression |
1 | | funres 5100 |
. . . . 5
⊢ (Fun
𝐴 → Fun (𝐴 ↾ 𝐵)) |
2 | | funfvex 5370 |
. . . . . 6
⊢ ((Fun
(𝐴 ↾ 𝐵) ∧ 𝑥 ∈ dom (𝐴 ↾ 𝐵)) → ((𝐴 ↾ 𝐵)‘𝑥) ∈ V) |
3 | 2 | ralrimiva 2464 |
. . . . 5
⊢ (Fun
(𝐴 ↾ 𝐵) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)((𝐴 ↾ 𝐵)‘𝑥) ∈ V) |
4 | | fnasrng 5532 |
. . . . 5
⊢
(∀𝑥 ∈
dom (𝐴 ↾ 𝐵)((𝐴 ↾ 𝐵)‘𝑥) ∈ V → (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) |
5 | 1, 3, 4 | 3syl 17 |
. . . 4
⊢ (Fun
𝐴 → (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) |
6 | 5 | adantr 272 |
. . 3
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) |
7 | 1 | adantr 272 |
. . . . 5
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → Fun (𝐴 ↾ 𝐵)) |
8 | | funfn 5089 |
. . . . 5
⊢ (Fun
(𝐴 ↾ 𝐵) ↔ (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
9 | 7, 8 | sylib 121 |
. . . 4
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
10 | | dffn5im 5399 |
. . . 4
⊢ ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) → (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥))) |
11 | 9, 10 | syl 14 |
. . 3
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥))) |
12 | | imadmrn 4827 |
. . . . 5
⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) |
13 | | vex 2644 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
14 | | opexg 4088 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ ((𝐴 ↾ 𝐵)‘𝑥) ∈ V) → 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉 ∈ V) |
15 | 13, 2, 14 | sylancr 408 |
. . . . . . . 8
⊢ ((Fun
(𝐴 ↾ 𝐵) ∧ 𝑥 ∈ dom (𝐴 ↾ 𝐵)) → 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉 ∈ V) |
16 | 15 | ralrimiva 2464 |
. . . . . . 7
⊢ (Fun
(𝐴 ↾ 𝐵) → ∀𝑥 ∈ dom (𝐴 ↾ 𝐵)〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉 ∈ V) |
17 | | dmmptg 4972 |
. . . . . . 7
⊢
(∀𝑥 ∈
dom (𝐴 ↾ 𝐵)〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉 ∈ V → dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) = dom (𝐴 ↾ 𝐵)) |
18 | 1, 16, 17 | 3syl 17 |
. . . . . 6
⊢ (Fun
𝐴 → dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) = dom (𝐴 ↾ 𝐵)) |
19 | 18 | imaeq2d 4817 |
. . . . 5
⊢ (Fun
𝐴 → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵))) |
20 | 12, 19 | syl5reqr 2147 |
. . . 4
⊢ (Fun
𝐴 → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) |
21 | 20 | adantr 272 |
. . 3
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) |
22 | 6, 11, 21 | 3eqtr4d 2142 |
. 2
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵))) |
23 | | funmpt 5097 |
. . 3
⊢ Fun
(𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) |
24 | | dmresexg 4778 |
. . . 4
⊢ (𝐵 ∈ 𝐶 → dom (𝐴 ↾ 𝐵) ∈ V) |
25 | 24 | adantl 273 |
. . 3
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → dom (𝐴 ↾ 𝐵) ∈ V) |
26 | | funimaexg 5143 |
. . 3
⊢ ((Fun
(𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) ∧ dom (𝐴 ↾ 𝐵) ∈ V) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) ∈ V) |
27 | 23, 25, 26 | sylancr 408 |
. 2
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) ∈ V) |
28 | 22, 27 | eqeltrd 2176 |
1
⊢ ((Fun
𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) |