Step | Hyp | Ref
| Expression |
1 | | funres 4884 |
. . . . 5
⊢ (Fun
A → Fun (A ↾ B)) |
2 | | funfvex 5135 |
. . . . . 6
⊢ ((Fun
(A ↾ B) ∧ x ∈ dom (A ↾ B))
→ ((A ↾ B)‘x)
∈ V) |
3 | 2 | ralrimiva 2386 |
. . . . 5
⊢ (Fun
(A ↾ B) → ∀x ∈ dom (A
↾ B)((A ↾ B)‘x)
∈ V) |
4 | | fnasrng 5286 |
. . . . 5
⊢ (∀x ∈ dom (A
↾ B)((A ↾ B)‘x)
∈ V → (x ∈ dom (A ↾ B)
↦ ((A ↾ B)‘x)) =
ran (x ∈
dom (A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉)) |
5 | 1, 3, 4 | 3syl 17 |
. . . 4
⊢ (Fun
A → (x ∈ dom (A ↾ B)
↦ ((A ↾ B)‘x)) =
ran (x ∈
dom (A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉)) |
6 | 5 | adantr 261 |
. . 3
⊢ ((Fun
A ∧
B ∈ 𝐶) → (x ∈ dom (A ↾ B)
↦ ((A ↾ B)‘x)) =
ran (x ∈
dom (A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉)) |
7 | 1 | adantr 261 |
. . . . 5
⊢ ((Fun
A ∧
B ∈ 𝐶) → Fun (A ↾ B)) |
8 | | funfn 4874 |
. . . . 5
⊢ (Fun
(A ↾ B) ↔ (A
↾ B) Fn dom (A ↾ B)) |
9 | 7, 8 | sylib 127 |
. . . 4
⊢ ((Fun
A ∧
B ∈ 𝐶) → (A ↾ B) Fn
dom (A ↾ B)) |
10 | | dffn5im 5162 |
. . . 4
⊢
((A ↾ B) Fn dom (A
↾ B) → (A ↾ B) =
(x ∈ dom
(A ↾ B) ↦ ((A
↾ B)‘x))) |
11 | 9, 10 | syl 14 |
. . 3
⊢ ((Fun
A ∧
B ∈ 𝐶) → (A ↾ B) =
(x ∈ dom
(A ↾ B) ↦ ((A
↾ B)‘x))) |
12 | | imadmrn 4621 |
. . . . 5
⊢
((x ∈ dom (A
↾ B) ↦ 〈x, ((A ↾
B)‘x)〉) “ dom (x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉)) = ran (x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉) |
13 | | vex 2554 |
. . . . . . . . 9
⊢ x ∈
V |
14 | | opexgOLD 3956 |
. . . . . . . . 9
⊢
((x ∈ V ∧ ((A ↾ B)‘x)
∈ V) → 〈x, ((A ↾
B)‘x)〉 ∈
V) |
15 | 13, 2, 14 | sylancr 393 |
. . . . . . . 8
⊢ ((Fun
(A ↾ B) ∧ x ∈ dom (A ↾ B))
→ 〈x, ((A ↾ B)‘x)〉 ∈
V) |
16 | 15 | ralrimiva 2386 |
. . . . . . 7
⊢ (Fun
(A ↾ B) → ∀x ∈ dom (A
↾ B)〈x, ((A ↾
B)‘x)〉 ∈
V) |
17 | | dmmptg 4761 |
. . . . . . 7
⊢ (∀x ∈ dom (A
↾ B)〈x, ((A ↾
B)‘x)〉 ∈ V
→ dom (x ∈ dom (A
↾ B) ↦ 〈x, ((A ↾
B)‘x)〉) = dom (A ↾ B)) |
18 | 1, 16, 17 | 3syl 17 |
. . . . . 6
⊢ (Fun
A → dom (x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉) = dom (A ↾ B)) |
19 | 18 | imaeq2d 4611 |
. . . . 5
⊢ (Fun
A → ((x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉) “ dom (x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉)) = ((x
∈ dom (A
↾ B) ↦ 〈x, ((A ↾
B)‘x)〉) “ dom (A ↾ B))) |
20 | 12, 19 | syl5reqr 2084 |
. . . 4
⊢ (Fun
A → ((x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉) “ dom (A ↾ B)) =
ran (x ∈
dom (A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉)) |
21 | 20 | adantr 261 |
. . 3
⊢ ((Fun
A ∧
B ∈ 𝐶) → ((x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉) “ dom (A ↾ B)) =
ran (x ∈
dom (A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉)) |
22 | 6, 11, 21 | 3eqtr4d 2079 |
. 2
⊢ ((Fun
A ∧
B ∈ 𝐶) → (A ↾ B) =
((x ∈ dom
(A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉) “ dom (A ↾ B))) |
23 | | funmpt 4881 |
. . 3
⊢ Fun
(x ∈ dom
(A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉) |
24 | | dmresexg 4577 |
. . . 4
⊢ (B ∈ 𝐶 → dom (A ↾ B)
∈ V) |
25 | 24 | adantl 262 |
. . 3
⊢ ((Fun
A ∧
B ∈ 𝐶) → dom (A ↾ B)
∈ V) |
26 | | funimaexg 4926 |
. . 3
⊢ ((Fun
(x ∈ dom
(A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉) ∧ dom
(A ↾ B) ∈ V) →
((x ∈ dom
(A ↾ B) ↦ 〈x, ((A ↾
B)‘x)〉) “ dom (A ↾ B))
∈ V) |
27 | 23, 25, 26 | sylancr 393 |
. 2
⊢ ((Fun
A ∧
B ∈ 𝐶) → ((x ∈ dom (A ↾ B)
↦ 〈x, ((A ↾ B)‘x)〉) “ dom (A ↾ B))
∈ V) |
28 | 22, 27 | eqeltrd 2111 |
1
⊢ ((Fun
A ∧
B ∈ 𝐶) → (A ↾ B)
∈ V) |