Proof of Theorem resdif
Step | Hyp | Ref
| Expression |
1 | | fofun 5270 |
. . . . . 6
⊢ ((F ↾ A):A–onto→C
→ Fun (F ↾ A)) |
2 | | difss 3393 |
. . . . . . 7
⊢ (A ∖ B) ⊆ A |
3 | | fof 5269 |
. . . . . . . 8
⊢ ((F ↾ A):A–onto→C
→ (F ↾ A):A–→C) |
4 | | fdm 5226 |
. . . . . . . 8
⊢ ((F ↾ A):A–→C
→ dom (F ↾ A) =
A) |
5 | 3, 4 | syl 15 |
. . . . . . 7
⊢ ((F ↾ A):A–onto→C
→ dom (F ↾ A) =
A) |
6 | 2, 5 | syl5sseqr 3320 |
. . . . . 6
⊢ ((F ↾ A):A–onto→C
→ (A ∖ B) ⊆ dom (F ↾ A)) |
7 | | fores 5278 |
. . . . . 6
⊢ ((Fun (F ↾ A) ∧ (A ∖ B) ⊆ dom
(F ↾
A)) → ((F ↾ A) ↾ (A ∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B))) |
8 | 1, 6, 7 | syl2anc 642 |
. . . . 5
⊢ ((F ↾ A):A–onto→C
→ ((F ↾ A) ↾ (A ∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B))) |
9 | | resabs1 4992 |
. . . . . . . 8
⊢ ((A ∖ B) ⊆ A → ((F
↾ A)
↾ (A
∖ B)) =
(F ↾
(A ∖
B))) |
10 | 2, 9 | ax-mp 5 |
. . . . . . 7
⊢ ((F ↾ A) ↾ (A ∖ B)) = (F ↾ (A ∖ B)) |
11 | | foeq1 5265 |
. . . . . . 7
⊢ (((F ↾ A) ↾ (A ∖ B)) = (F ↾ (A ∖ B)) →
(((F ↾
A) ↾
(A ∖
B)):(A
∖ B)–onto→((F ↾ A) “
(A ∖
B)) ↔ (F ↾ (A ∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B)))) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ (((F ↾ A) ↾ (A ∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B)) ↔ (F ↾ (A ∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B))) |
13 | 10 | rneqi 4957 |
. . . . . . . 8
⊢ ran ((F ↾ A) ↾ (A ∖ B)) = ran (F
↾ (A
∖ B)) |
14 | | dfima3 4951 |
. . . . . . . 8
⊢ ((F ↾ A) “ (A
∖ B)) =
ran ((F ↾ A) ↾ (A ∖ B)) |
15 | | dfima3 4951 |
. . . . . . . 8
⊢ (F “ (A
∖ B)) =
ran (F ↾
(A ∖
B)) |
16 | 13, 14, 15 | 3eqtr4i 2383 |
. . . . . . 7
⊢ ((F ↾ A) “ (A
∖ B)) =
(F “ (A ∖ B)) |
17 | | foeq3 5267 |
. . . . . . 7
⊢ (((F ↾ A) “ (A
∖ B)) =
(F “ (A ∖ B)) → ((F
↾ (A
∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B)) ↔ (F ↾ (A ∖ B)):(A ∖ B)–onto→(F “
(A ∖
B)))) |
18 | 16, 17 | ax-mp 5 |
. . . . . 6
⊢ ((F ↾ (A ∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B)) ↔ (F ↾ (A ∖ B)):(A ∖ B)–onto→(F “
(A ∖
B))) |
19 | 12, 18 | bitri 240 |
. . . . 5
⊢ (((F ↾ A) ↾ (A ∖ B)):(A ∖ B)–onto→((F ↾ A) “
(A ∖
B)) ↔ (F ↾ (A ∖ B)):(A ∖ B)–onto→(F “
(A ∖
B))) |
20 | 8, 19 | sylib 188 |
. . . 4
⊢ ((F ↾ A):A–onto→C
→ (F ↾ (A ∖ B)):(A ∖ B)–onto→(F “
(A ∖
B))) |
21 | | funres11 5164 |
. . . 4
⊢ (Fun ◡F →
Fun ◡(F ↾ (A ∖ B))) |
22 | | dff1o3 5292 |
. . . . 5
⊢ ((F ↾ (A ∖ B)):(A ∖ B)–1-1-onto→(F “
(A ∖
B)) ↔ ((F ↾ (A ∖ B)):(A ∖ B)–onto→(F “
(A ∖
B)) ∧ Fun
◡(F
↾ (A
∖ B)))) |
23 | 22 | biimpri 197 |
. . . 4
⊢ (((F ↾ (A ∖ B)):(A ∖ B)–onto→(F “
(A ∖
B)) ∧ Fun
◡(F
↾ (A
∖ B)))
→ (F ↾ (A ∖ B)):(A ∖ B)–1-1-onto→(F “
(A ∖
B))) |
24 | 20, 21, 23 | syl2anr 464 |
. . 3
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C) →
(F ↾
(A ∖
B)):(A
∖ B)–1-1-onto→(F “
(A ∖
B))) |
25 | 24 | 3adant3 975 |
. 2
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
(F ↾
(A ∖
B)):(A
∖ B)–1-1-onto→(F “
(A ∖
B))) |
26 | | dfima3 4951 |
. . . . . . 7
⊢ (F “ A) =
ran (F ↾
A) |
27 | | forn 5272 |
. . . . . . 7
⊢ ((F ↾ A):A–onto→C
→ ran (F ↾ A) =
C) |
28 | 26, 27 | syl5eq 2397 |
. . . . . 6
⊢ ((F ↾ A):A–onto→C
→ (F “ A) = C) |
29 | | dfima3 4951 |
. . . . . . 7
⊢ (F “ B) =
ran (F ↾
B) |
30 | | forn 5272 |
. . . . . . 7
⊢ ((F ↾ B):B–onto→D
→ ran (F ↾ B) =
D) |
31 | 29, 30 | syl5eq 2397 |
. . . . . 6
⊢ ((F ↾ B):B–onto→D
→ (F “ B) = D) |
32 | 28, 31 | anim12i 549 |
. . . . 5
⊢ (((F ↾ A):A–onto→C
∧ (F ↾ B):B–onto→D) →
((F “ A) = C ∧ (F “
B) = D)) |
33 | | imadif 5171 |
. . . . . 6
⊢ (Fun ◡F →
(F “ (A ∖ B)) = ((F
“ A) ∖ (F “
B))) |
34 | | difeq12 3380 |
. . . . . 6
⊢ (((F “ A) =
C ∧
(F “ B) = D) →
((F “ A) ∖ (F “ B)) =
(C ∖
D)) |
35 | 33, 34 | sylan9eq 2405 |
. . . . 5
⊢ ((Fun ◡F ∧ ((F “
A) = C
∧ (F
“ B) = D)) → (F
“ (A ∖ B)) =
(C ∖
D)) |
36 | 32, 35 | sylan2 460 |
. . . 4
⊢ ((Fun ◡F ∧ ((F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D)) →
(F “ (A ∖ B)) = (C ∖ D)) |
37 | 36 | 3impb 1147 |
. . 3
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
(F “ (A ∖ B)) = (C ∖ D)) |
38 | | f1oeq3 5283 |
. . 3
⊢ ((F “ (A
∖ B)) =
(C ∖
D) → ((F ↾ (A ∖ B)):(A ∖ B)–1-1-onto→(F “
(A ∖
B)) ↔ (F ↾ (A ∖ B)):(A ∖ B)–1-1-onto→(C ∖ D))) |
39 | 37, 38 | syl 15 |
. 2
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
((F ↾
(A ∖
B)):(A
∖ B)–1-1-onto→(F “
(A ∖
B)) ↔ (F ↾ (A ∖ B)):(A ∖ B)–1-1-onto→(C ∖ D))) |
40 | 25, 39 | mpbid 201 |
1
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
(F ↾
(A ∖
B)):(A
∖ B)–1-1-onto→(C ∖ D)) |