Proof of Theorem foimacnv
| Step | Hyp | Ref
| Expression |
| 1 | | resima 6033 |
. 2
⊢ ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = (𝐹 “ (◡𝐹 “ 𝐶)) |
| 2 | | fofun 6821 |
. . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
| 3 | 2 | adantr 480 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun 𝐹) |
| 4 | | funcnvres2 6646 |
. . . . 5
⊢ (Fun
𝐹 → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
| 6 | 5 | imaeq1d 6077 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶))) |
| 7 | | resss 6019 |
. . . . . . . . . 10
⊢ (◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 |
| 8 | | cnvss 5883 |
. . . . . . . . . 10
⊢ ((◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 → ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹 |
| 10 | | cnvcnvss 6214 |
. . . . . . . . 9
⊢ ◡◡𝐹 ⊆ 𝐹 |
| 11 | 9, 10 | sstri 3993 |
. . . . . . . 8
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 |
| 12 | | funss 6585 |
. . . . . . . 8
⊢ (◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun ◡(◡𝐹 ↾ 𝐶))) |
| 13 | 11, 2, 12 | mpsyl 68 |
. . . . . . 7
⊢ (𝐹:𝐴–onto→𝐵 → Fun ◡(◡𝐹 ↾ 𝐶)) |
| 14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun ◡(◡𝐹 ↾ 𝐶)) |
| 15 | | df-ima 5698 |
. . . . . . 7
⊢ (◡𝐹 “ 𝐶) = ran (◡𝐹 ↾ 𝐶) |
| 16 | | df-rn 5696 |
. . . . . . 7
⊢ ran
(◡𝐹 ↾ 𝐶) = dom ◡(◡𝐹 ↾ 𝐶) |
| 17 | 15, 16 | eqtr2i 2766 |
. . . . . 6
⊢ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶) |
| 18 | | df-fn 6564 |
. . . . . 6
⊢ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ↔ (Fun ◡(◡𝐹 ↾ 𝐶) ∧ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶))) |
| 19 | 14, 17, 18 | sylanblrc 590 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶)) |
| 20 | | dfdm4 5906 |
. . . . . 6
⊢ dom
(◡𝐹 ↾ 𝐶) = ran ◡(◡𝐹 ↾ 𝐶) |
| 21 | | forn 6823 |
. . . . . . . . . 10
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
| 22 | 21 | sseq2d 4016 |
. . . . . . . . 9
⊢ (𝐹:𝐴–onto→𝐵 → (𝐶 ⊆ ran 𝐹 ↔ 𝐶 ⊆ 𝐵)) |
| 23 | 22 | biimpar 477 |
. . . . . . . 8
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ ran 𝐹) |
| 24 | | df-rn 5696 |
. . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 |
| 25 | 23, 24 | sseqtrdi 4024 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ dom ◡𝐹) |
| 26 | | ssdmres 6031 |
. . . . . . 7
⊢ (𝐶 ⊆ dom ◡𝐹 ↔ dom (◡𝐹 ↾ 𝐶) = 𝐶) |
| 27 | 25, 26 | sylib 218 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → dom (◡𝐹 ↾ 𝐶) = 𝐶) |
| 28 | 20, 27 | eqtr3id 2791 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ran ◡(◡𝐹 ↾ 𝐶) = 𝐶) |
| 29 | | df-fo 6567 |
. . . . 5
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 ↔ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ∧ ran ◡(◡𝐹 ↾ 𝐶) = 𝐶)) |
| 30 | 19, 28, 29 | sylanbrc 583 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶) |
| 31 | | foima 6825 |
. . . 4
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
| 32 | 30, 31 | syl 17 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
| 33 | 6, 32 | eqtr3d 2779 |
. 2
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = 𝐶) |
| 34 | 1, 33 | eqtr3id 2791 |
1
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶) |