Metamath Proof Explorer

Theorem focofo

Description: Composition of onto functions. Generalisation of foco . (Contributed by AV, 29-Sep-2024)

Ref Expression
Assertion focofo ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) –onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 fcof ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 )
3 1 2 sylan ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 )
4 3 3adant3 ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 )
5 rnco ⊢ ran ( 𝐹 ∘ 𝐺 ) = ran ( 𝐹 ↾ ran 𝐺 )
6 1 freld ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Rel 𝐹 )
7 6 3ad2ant1 ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → Rel 𝐹 )
8 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
9 8 eqcomd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 = dom 𝐹 )
10 1 9 syl ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐴 = dom 𝐹 )
11 10 sseq1d ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐴 ⊆ ran 𝐺 ↔ dom 𝐹 ⊆ ran 𝐺 ) )
12 11 biimpa ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐴 ⊆ ran 𝐺 ) → dom 𝐹 ⊆ ran 𝐺 )
13 relssres ⊢ ( ( Rel 𝐹 ∧ dom 𝐹 ⊆ ran 𝐺 ) → ( 𝐹 ↾ ran 𝐺 ) = 𝐹 )
14 13 rneqd ⊢ ( ( Rel 𝐹 ∧ dom 𝐹 ⊆ ran 𝐺 ) → ran ( 𝐹 ↾ ran 𝐺 ) = ran 𝐹 )
15 7 12 14 3imp3i2an ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → ran ( 𝐹 ↾ ran 𝐺 ) = ran 𝐹 )
16 forn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
17 16 3ad2ant1 ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → ran 𝐹 = 𝐵 )
18 15 17 eqtrd ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → ran ( 𝐹 ↾ ran 𝐺 ) = 𝐵 )
19 5 18 syl5eq ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → ran ( 𝐹 ∘ 𝐺 ) = 𝐵 )
20 dffo2 ⊢ ( ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) –onto→ 𝐵 ↔ ( ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) ⟶ 𝐵 ∧ ran ( 𝐹 ∘ 𝐺 ) = 𝐵 ) )
21 4 19 20 sylanbrc ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ) → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ 𝐴 ) –onto→ 𝐵 )