Proof of Theorem foimacnv
Step | Hyp | Ref
| Expression |
1 | | resima 5351 |
. 2
⊢ ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = (𝐹 “ (◡𝐹 “ 𝐶)) |
2 | | fofun 6029 |
. . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
3 | 2 | adantr 480 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun 𝐹) |
4 | | funcnvres2 5883 |
. . . . 5
⊢ (Fun
𝐹 → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
6 | 5 | imaeq1d 5384 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶))) |
7 | | resss 5342 |
. . . . . . . . . . 11
⊢ (◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 |
8 | | cnvss 5216 |
. . . . . . . . . . 11
⊢ ((◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 → ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹 |
10 | | cnvcnvss 5507 |
. . . . . . . . . 10
⊢ ◡◡𝐹 ⊆ 𝐹 |
11 | 9, 10 | sstri 3577 |
. . . . . . . . 9
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 |
12 | | funss 5822 |
. . . . . . . . 9
⊢ (◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun ◡(◡𝐹 ↾ 𝐶))) |
13 | 11, 2, 12 | mpsyl 66 |
. . . . . . . 8
⊢ (𝐹:𝐴–onto→𝐵 → Fun ◡(◡𝐹 ↾ 𝐶)) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun ◡(◡𝐹 ↾ 𝐶)) |
15 | | df-ima 5051 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝐶) = ran (◡𝐹 ↾ 𝐶) |
16 | | df-rn 5049 |
. . . . . . . 8
⊢ ran
(◡𝐹 ↾ 𝐶) = dom ◡(◡𝐹 ↾ 𝐶) |
17 | 15, 16 | eqtr2i 2633 |
. . . . . . 7
⊢ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶) |
18 | 14, 17 | jctir 559 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (Fun ◡(◡𝐹 ↾ 𝐶) ∧ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶))) |
19 | | df-fn 5807 |
. . . . . 6
⊢ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ↔ (Fun ◡(◡𝐹 ↾ 𝐶) ∧ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶))) |
20 | 18, 19 | sylibr 223 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶)) |
21 | | dfdm4 5238 |
. . . . . 6
⊢ dom
(◡𝐹 ↾ 𝐶) = ran ◡(◡𝐹 ↾ 𝐶) |
22 | | forn 6031 |
. . . . . . . . . 10
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
23 | 22 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝐹:𝐴–onto→𝐵 → (𝐶 ⊆ ran 𝐹 ↔ 𝐶 ⊆ 𝐵)) |
24 | 23 | biimpar 501 |
. . . . . . . 8
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ ran 𝐹) |
25 | | df-rn 5049 |
. . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 |
26 | 24, 25 | syl6sseq 3614 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ dom ◡𝐹) |
27 | | ssdmres 5340 |
. . . . . . 7
⊢ (𝐶 ⊆ dom ◡𝐹 ↔ dom (◡𝐹 ↾ 𝐶) = 𝐶) |
28 | 26, 27 | sylib 207 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → dom (◡𝐹 ↾ 𝐶) = 𝐶) |
29 | 21, 28 | syl5eqr 2658 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ran ◡(◡𝐹 ↾ 𝐶) = 𝐶) |
30 | | df-fo 5810 |
. . . . 5
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 ↔ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ∧ ran ◡(◡𝐹 ↾ 𝐶) = 𝐶)) |
31 | 20, 29, 30 | sylanbrc 695 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶) |
32 | | foima 6033 |
. . . 4
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
33 | 31, 32 | syl 17 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
34 | 6, 33 | eqtr3d 2646 |
. 2
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = 𝐶) |
35 | 1, 34 | syl5eqr 2658 |
1
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶) |