Proof of Theorem foimacnv
Step | Hyp | Ref
| Expression |
1 | | resima 4691 |
. 2
⊢ ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = (𝐹 “ (◡𝐹 “ 𝐶)) |
2 | | fofun 5158 |
. . . . . 6
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
3 | 2 | adantr 270 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun 𝐹) |
4 | | funcnvres2 5025 |
. . . . 5
⊢ (Fun
𝐹 → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
5 | 3, 4 | syl 14 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶))) |
6 | 5 | imaeq1d 4717 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶))) |
7 | | resss 4683 |
. . . . . . . . . . 11
⊢ (◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 |
8 | | cnvss 4556 |
. . . . . . . . . . 11
⊢ ((◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 → ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹) |
9 | 7, 8 | ax-mp 7 |
. . . . . . . . . 10
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹 |
10 | | cnvcnvss 4825 |
. . . . . . . . . 10
⊢ ◡◡𝐹 ⊆ 𝐹 |
11 | 9, 10 | sstri 3017 |
. . . . . . . . 9
⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 |
12 | | funss 4970 |
. . . . . . . . 9
⊢ (◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun ◡(◡𝐹 ↾ 𝐶))) |
13 | 11, 2, 12 | mpsyl 64 |
. . . . . . . 8
⊢ (𝐹:𝐴–onto→𝐵 → Fun ◡(◡𝐹 ↾ 𝐶)) |
14 | 13 | adantr 270 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun ◡(◡𝐹 ↾ 𝐶)) |
15 | | df-ima 4404 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝐶) = ran (◡𝐹 ↾ 𝐶) |
16 | | df-rn 4402 |
. . . . . . . 8
⊢ ran
(◡𝐹 ↾ 𝐶) = dom ◡(◡𝐹 ↾ 𝐶) |
17 | 15, 16 | eqtr2i 2104 |
. . . . . . 7
⊢ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶) |
18 | 14, 17 | jctir 306 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (Fun ◡(◡𝐹 ↾ 𝐶) ∧ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶))) |
19 | | df-fn 4955 |
. . . . . 6
⊢ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ↔ (Fun ◡(◡𝐹 ↾ 𝐶) ∧ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶))) |
20 | 18, 19 | sylibr 132 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶)) |
21 | | dfdm4 4575 |
. . . . . 6
⊢ dom
(◡𝐹 ↾ 𝐶) = ran ◡(◡𝐹 ↾ 𝐶) |
22 | | forn 5160 |
. . . . . . . . . 10
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
23 | 22 | sseq2d 3036 |
. . . . . . . . 9
⊢ (𝐹:𝐴–onto→𝐵 → (𝐶 ⊆ ran 𝐹 ↔ 𝐶 ⊆ 𝐵)) |
24 | 23 | biimpar 291 |
. . . . . . . 8
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ ran 𝐹) |
25 | | df-rn 4402 |
. . . . . . . 8
⊢ ran 𝐹 = dom ◡𝐹 |
26 | 24, 25 | syl6sseq 3054 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ dom ◡𝐹) |
27 | | ssdmres 4681 |
. . . . . . 7
⊢ (𝐶 ⊆ dom ◡𝐹 ↔ dom (◡𝐹 ↾ 𝐶) = 𝐶) |
28 | 26, 27 | sylib 120 |
. . . . . 6
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → dom (◡𝐹 ↾ 𝐶) = 𝐶) |
29 | 21, 28 | syl5eqr 2129 |
. . . . 5
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ran ◡(◡𝐹 ↾ 𝐶) = 𝐶) |
30 | | df-fo 4958 |
. . . . 5
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 ↔ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ∧ ran ◡(◡𝐹 ↾ 𝐶) = 𝐶)) |
31 | 20, 29, 30 | sylanbrc 408 |
. . . 4
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶) |
32 | | foima 5162 |
. . . 4
⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
33 | 31, 32 | syl 14 |
. . 3
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶) |
34 | 6, 33 | eqtr3d 2117 |
. 2
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = 𝐶) |
35 | 1, 34 | syl5eqr 2129 |
1
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶) |