Step | Hyp | Ref
| Expression |
1 | | dffun2 5119 |
. . . 4
⊢ (Fun (F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F))) ↔
∀x∀y∀z((x(F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F)))y ∧ x(F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F)))z) → y =
z)) |
2 | | brres 4949 |
. . . . . . 7
⊢ (x(F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F)))y ↔
(xFy ∧ x ∈ dom (( I ∘
F) ∖ (
∼ I ∘ F)))) |
3 | | fvfullfunlem1 5861 |
. . . . . . . . 9
⊢ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) = {x ∣ ∃!z xFz} |
4 | 3 | abeq2i 2460 |
. . . . . . . 8
⊢ (x ∈ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) ↔ ∃!z xFz) |
5 | 4 | anbi2i 675 |
. . . . . . 7
⊢ ((xFy ∧ x ∈ dom (( I ∘ F) ∖ ( ∼ I ∘
F))) ↔ (xFy ∧ ∃!z xFz)) |
6 | 2, 5 | bitri 240 |
. . . . . 6
⊢ (x(F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F)))y ↔
(xFy ∧ ∃!z xFz)) |
7 | | brres 4949 |
. . . . . . 7
⊢ (x(F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F)))z ↔
(xFz ∧ x ∈ dom (( I ∘
F) ∖ (
∼ I ∘ F)))) |
8 | | fvfullfunlem1 5861 |
. . . . . . . . 9
⊢ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) = {x ∣ ∃!y xFy} |
9 | 8 | abeq2i 2460 |
. . . . . . . 8
⊢ (x ∈ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) ↔ ∃!y xFy) |
10 | 9 | anbi2i 675 |
. . . . . . 7
⊢ ((xFz ∧ x ∈ dom (( I ∘ F) ∖ ( ∼ I ∘
F))) ↔ (xFz ∧ ∃!y xFy)) |
11 | 7, 10 | bitri 240 |
. . . . . 6
⊢ (x(F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F)))z ↔
(xFz ∧ ∃!y xFy)) |
12 | | tz6.12-1 5344 |
. . . . . . . . 9
⊢ ((xFy ∧ ∃!y xFy) → (F
‘x) = y) |
13 | 12 | adantrl 696 |
. . . . . . . 8
⊢ ((xFy ∧ (xFz ∧ ∃!y xFy)) → (F
‘x) = y) |
14 | | tz6.12-1 5344 |
. . . . . . . . 9
⊢ ((xFz ∧ ∃!y xFy) → (F
‘x) = z) |
15 | 14 | adantl 452 |
. . . . . . . 8
⊢ ((xFy ∧ (xFz ∧ ∃!y xFy)) → (F
‘x) = z) |
16 | 13, 15 | eqtr3d 2387 |
. . . . . . 7
⊢ ((xFy ∧ (xFz ∧ ∃!y xFy)) → y =
z) |
17 | 16 | adantlr 695 |
. . . . . 6
⊢ (((xFy ∧ ∃!z xFz) ∧ (xFz ∧ ∃!y xFy)) → y =
z) |
18 | 6, 11, 17 | syl2anb 465 |
. . . . 5
⊢ ((x(F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F)))y ∧ x(F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F)))z) → y =
z) |
19 | 18 | gen2 1547 |
. . . 4
⊢ ∀y∀z((x(F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F)))y ∧ x(F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F)))z) → y =
z) |
20 | 1, 19 | mpgbir 1550 |
. . 3
⊢ Fun (F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F))) |
21 | | fvfullfunlem2 5862 |
. . . . 5
⊢ (( I ∘ F) ∖ ( ∼ I ∘
F)) ⊆
F |
22 | | ssdmrn 5099 |
. . . . . 6
⊢ (( I ∘ F) ∖ ( ∼ I ∘
F)) ⊆
(dom (( I ∘ F) ∖ ( ∼ I
∘ F))
× ran (( I ∘ F) ∖ ( ∼ I
∘ F))) |
23 | | ssv 3291 |
. . . . . . 7
⊢ ran (( I ∘ F) ∖ ( ∼ I ∘
F)) ⊆
V |
24 | | xpss2 4857 |
. . . . . . 7
⊢ (ran (( I ∘ F) ∖ ( ∼ I ∘
F)) ⊆ V
→ (dom (( I ∘ F) ∖ ( ∼ I
∘ F))
× ran (( I ∘ F) ∖ ( ∼ I
∘ F)))
⊆ (dom (( I ∘ F) ∖ ( ∼ I ∘
F)) × V)) |
25 | 23, 24 | ax-mp 5 |
. . . . . 6
⊢ (dom (( I ∘ F) ∖ ( ∼ I ∘
F)) × ran (( I ∘ F) ∖ ( ∼ I ∘
F))) ⊆
(dom (( I ∘ F) ∖ ( ∼ I
∘ F))
× V) |
26 | 22, 25 | sstri 3281 |
. . . . 5
⊢ (( I ∘ F) ∖ ( ∼ I ∘
F)) ⊆
(dom (( I ∘ F) ∖ ( ∼ I
∘ F))
× V) |
27 | 21, 26 | ssini 3478 |
. . . 4
⊢ (( I ∘ F) ∖ ( ∼ I ∘
F)) ⊆
(F ∩ (dom (( I ∘ F) ∖ ( ∼ I ∘
F)) × V)) |
28 | | df-res 4788 |
. . . 4
⊢ (F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F))) =
(F ∩ (dom (( I ∘ F) ∖ ( ∼ I ∘
F)) × V)) |
29 | 27, 28 | sseqtr4i 3304 |
. . 3
⊢ (( I ∘ F) ∖ ( ∼ I ∘
F)) ⊆
(F ↾ dom
(( I ∘ F) ∖ ( ∼ I
∘ F))) |
30 | | funssfv 5343 |
. . 3
⊢ ((Fun (F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F))) ∧ (( I ∘ F) ∖ ( ∼ I
∘ F))
⊆ (F
↾ dom (( I ∘ F) ∖ ( ∼ I ∘
F))) ∧
A ∈ dom
(( I ∘ F) ∖ ( ∼ I
∘ F)))
→ ((F ↾ dom (( I ∘
F) ∖ (
∼ I ∘ F))) ‘A) =
((( I ∘ F) ∖ ( ∼ I
∘ F))
‘A)) |
31 | 20, 29, 30 | mp3an12 1267 |
. 2
⊢ (A ∈ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) → ((F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F)))
‘A) = ((( I ∘ F) ∖ ( ∼ I ∘
F)) ‘A)) |
32 | | fvres 5342 |
. 2
⊢ (A ∈ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) → ((F ↾ dom (( I
∘ F)
∖ ( ∼ I ∘ F)))
‘A) = (F ‘A)) |
33 | 31, 32 | eqtr3d 2387 |
1
⊢ (A ∈ dom (( I ∘ F) ∖ ( ∼ I ∘
F)) → ((( I ∘ F) ∖ ( ∼ I ∘
F)) ‘A) = (F
‘A)) |