Proof of Theorem foco
Step | Hyp | Ref
| Expression |
1 | | dffo2 5053 |
. . 3
⊢ (𝐹:B–onto→𝐶 ↔ (𝐹:B⟶𝐶 ∧ ran
𝐹 = 𝐶)) |
2 | | dffo2 5053 |
. . 3
⊢ (𝐺:A–onto→B ↔
(𝐺:A⟶B ∧ ran 𝐺 = B)) |
3 | | fco 4999 |
. . . . 5
⊢ ((𝐹:B⟶𝐶 ∧ 𝐺:A⟶B)
→ (𝐹 ∘ 𝐺):A⟶𝐶) |
4 | 3 | ad2ant2r 478 |
. . . 4
⊢ (((𝐹:B⟶𝐶 ∧ ran
𝐹 = 𝐶) ∧ (𝐺:A⟶B ∧ ran 𝐺 = B))
→ (𝐹 ∘ 𝐺):A⟶𝐶) |
5 | | fdm 4993 |
. . . . . . . 8
⊢ (𝐹:B⟶𝐶 → dom 𝐹 = B) |
6 | | eqtr3 2056 |
. . . . . . . 8
⊢ ((dom
𝐹 = B ∧ ran 𝐺 = B) → dom 𝐹 = ran 𝐺) |
7 | 5, 6 | sylan 267 |
. . . . . . 7
⊢ ((𝐹:B⟶𝐶 ∧ ran
𝐺 = B) → dom 𝐹 = ran 𝐺) |
8 | | rncoeq 4548 |
. . . . . . . . 9
⊢ (dom
𝐹 = ran 𝐺 → ran (𝐹 ∘ 𝐺) = ran 𝐹) |
9 | 8 | eqeq1d 2045 |
. . . . . . . 8
⊢ (dom
𝐹 = ran 𝐺 → (ran (𝐹 ∘ 𝐺) = 𝐶 ↔ ran 𝐹 = 𝐶)) |
10 | 9 | biimpar 281 |
. . . . . . 7
⊢ ((dom
𝐹 = ran 𝐺 ∧ ran
𝐹 = 𝐶) → ran (𝐹 ∘ 𝐺) = 𝐶) |
11 | 7, 10 | sylan 267 |
. . . . . 6
⊢ (((𝐹:B⟶𝐶 ∧ ran
𝐺 = B) ∧ ran 𝐹 = 𝐶) → ran (𝐹 ∘ 𝐺) = 𝐶) |
12 | 11 | an32s 502 |
. . . . 5
⊢ (((𝐹:B⟶𝐶 ∧ ran
𝐹 = 𝐶) ∧ ran
𝐺 = B) → ran (𝐹 ∘ 𝐺) = 𝐶) |
13 | 12 | adantrl 447 |
. . . 4
⊢ (((𝐹:B⟶𝐶 ∧ ran
𝐹 = 𝐶) ∧ (𝐺:A⟶B ∧ ran 𝐺 = B))
→ ran (𝐹 ∘ 𝐺) = 𝐶) |
14 | 4, 13 | jca 290 |
. . 3
⊢ (((𝐹:B⟶𝐶 ∧ ran
𝐹 = 𝐶) ∧ (𝐺:A⟶B ∧ ran 𝐺 = B))
→ ((𝐹 ∘ 𝐺):A⟶𝐶 ∧ ran
(𝐹 ∘ 𝐺) = 𝐶)) |
15 | 1, 2, 14 | syl2anb 275 |
. 2
⊢ ((𝐹:B–onto→𝐶 ∧ 𝐺:A–onto→B) →
((𝐹 ∘ 𝐺):A⟶𝐶 ∧ ran
(𝐹 ∘ 𝐺) = 𝐶)) |
16 | | dffo2 5053 |
. 2
⊢ ((𝐹 ∘ 𝐺):A–onto→𝐶 ↔ ((𝐹 ∘ 𝐺):A⟶𝐶 ∧ ran
(𝐹 ∘ 𝐺) = 𝐶)) |
17 | 15, 16 | sylibr 137 |
1
⊢ ((𝐹:B–onto→𝐶 ∧ 𝐺:A–onto→B) →
(𝐹 ∘ 𝐺):A–onto→𝐶) |