Step |
Hyp |
Ref |
Expression |
1 |
|
dffo2 |
⊢ ( 𝐹 : 𝐵 –onto→ 𝐶 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ) |
2 |
|
dffo2 |
⊢ ( 𝐺 : 𝐴 –onto→ 𝐵 ↔ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) ) |
3 |
|
fco |
⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ) |
4 |
3
|
ad2ant2r |
⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ) |
5 |
|
fdm |
⊢ ( 𝐹 : 𝐵 ⟶ 𝐶 → dom 𝐹 = 𝐵 ) |
6 |
|
eqtr3 |
⊢ ( ( dom 𝐹 = 𝐵 ∧ ran 𝐺 = 𝐵 ) → dom 𝐹 = ran 𝐺 ) |
7 |
5 6
|
sylan |
⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐺 = 𝐵 ) → dom 𝐹 = ran 𝐺 ) |
8 |
|
rncoeq |
⊢ ( dom 𝐹 = ran 𝐺 → ran ( 𝐹 ∘ 𝐺 ) = ran 𝐹 ) |
9 |
8
|
eqeq1d |
⊢ ( dom 𝐹 = ran 𝐺 → ( ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ↔ ran 𝐹 = 𝐶 ) ) |
10 |
9
|
biimpar |
⊢ ( ( dom 𝐹 = ran 𝐺 ∧ ran 𝐹 = 𝐶 ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) |
11 |
7 10
|
sylan |
⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐺 = 𝐵 ) ∧ ran 𝐹 = 𝐶 ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) |
12 |
11
|
an32s |
⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ran 𝐺 = 𝐵 ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) |
13 |
12
|
adantrl |
⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) |
14 |
4 13
|
jca |
⊢ ( ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐶 ) ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ran 𝐺 = 𝐵 ) ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) ) |
15 |
1 2 14
|
syl2anb |
⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) ) |
16 |
|
dffo2 |
⊢ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ↔ ( ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ∧ ran ( 𝐹 ∘ 𝐺 ) = 𝐶 ) ) |
17 |
15 16
|
sylibr |
⊢ ( ( 𝐹 : 𝐵 –onto→ 𝐶 ∧ 𝐺 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) |