Proof of Theorem foimacnv
Step | Hyp | Ref
| Expression |
1 | | resima 5924 |
. 2
⊢ ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = (𝐹 “ (◡𝐹 “ 𝐶)) |
2 | | fofun 6687 |
. . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
3 | 2 | adantr 481 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun 𝐹) |
4 | | funcnvres2 6512 |
. . . . 5
⊢ (Fun
𝐹 → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
6 | 5 | imaeq1d 5967 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶))) |
7 | | resss 5915 |
. . . . . . . . . 10
⊢ (◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 |
8 | | cnvss 5780 |
. . . . . . . . . 10
⊢ ((◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 → ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹 |
10 | | cnvcnvss 6096 |
. . . . . . . . 9
⊢ ◡◡𝐹 ⊆ 𝐹 |
11 | 9, 10 | sstri 3935 |
. . . . . . . 8
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 |
12 | | funss 6451 |
. . . . . . . 8
⊢ (◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun ◡(◡𝐹 ↾ 𝐶))) |
13 | 11, 2, 12 | mpsyl 68 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→𝐵 → Fun ◡(◡𝐹 ↾ 𝐶)) |
14 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun ◡(◡𝐹 ↾ 𝐶)) |
15 | | df-ima 5603 |
. . . . . . 7
⊢ (◡𝐹 “ 𝐶) = ran (◡𝐹 ↾ 𝐶) |
16 | | df-rn 5601 |
. . . . . . 7
⊢ ran
(◡𝐹 ↾ 𝐶) = dom ◡(◡𝐹 ↾ 𝐶) |
17 | 15, 16 | eqtr2i 2769 |
. . . . . 6
⊢ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶) |
18 | | df-fn 6435 |
. . . . . 6
⊢ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ↔ (Fun ◡(◡𝐹 ↾ 𝐶) ∧ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶))) |
19 | 14, 17, 18 | sylanblrc 590 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶)) |
20 | | dfdm4 5803 |
. . . . . 6
⊢ dom
(◡𝐹 ↾ 𝐶) = ran ◡(◡𝐹 ↾ 𝐶) |
21 | | forn 6689 |
. . . . . . . . . 10
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
22 | 21 | sseq2d 3958 |
. . . . . . . . 9
⊢ (𝐹:𝐴–onto→𝐵 → (𝐶 ⊆ ran 𝐹 ↔ 𝐶 ⊆ 𝐵)) |
23 | 22 | biimpar 478 |
. . . . . . . 8
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ ran 𝐹) |
24 | | df-rn 5601 |
. . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 |
25 | 23, 24 | sseqtrdi 3976 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ dom ◡𝐹) |
26 | | ssdmres 5913 |
. . . . . . 7
⊢ (𝐶 ⊆ dom ◡𝐹 ↔ dom (◡𝐹 ↾ 𝐶) = 𝐶) |
27 | 25, 26 | sylib 217 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → dom (◡𝐹 ↾ 𝐶) = 𝐶) |
28 | 20, 27 | eqtr3id 2794 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ran ◡(◡𝐹 ↾ 𝐶) = 𝐶) |
29 | | df-fo 6438 |
. . . . 5
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 ↔ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ∧ ran ◡(◡𝐹 ↾ 𝐶) = 𝐶)) |
30 | 19, 28, 29 | sylanbrc 583 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶) |
31 | | foima 6691 |
. . . 4
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
32 | 30, 31 | syl 17 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
33 | 6, 32 | eqtr3d 2782 |
. 2
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = 𝐶) |
34 | 1, 33 | eqtr3id 2794 |
1
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶) |