Metamath Proof Explorer

Theorem fnfocofob

Description: If the domain of a function G equals the range of a function F , then the composition ( G o. F ) is surjective iff G is surjective. (Contributed by GL and AV, 29-Sep-2024)

Ref Expression
Assertion fnfocofob ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → G ∘ F : A ⟶ onto C ↔ G : B ⟶ onto C

Proof

Step Hyp Ref Expression
1 cnvimarndm ⊢ F -1 ran ⁡ F = dom ⁡ F
2 fndm ⊢ F Fn A → dom ⁡ F = A
3 2 3ad2ant1 ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → dom ⁡ F = A
4 1 3 eqtr2id ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → A = F -1 ran ⁡ F
5 imaeq2 ⊢ ran ⁡ F = B → F -1 ran ⁡ F = F -1 B
6 5 3ad2ant3 ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → F -1 ran ⁡ F = F -1 B
7 4 6 eqtrd ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → A = F -1 B
8 foeq2 ⊢ A = F -1 B → G ∘ F : A ⟶ onto C ↔ G ∘ F : F -1 B ⟶ onto C
9 7 8 syl ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → G ∘ F : A ⟶ onto C ↔ G ∘ F : F -1 B ⟶ onto C
10 fnfun ⊢ F Fn A → Fun ⁡ F
11 id ⊢ G : B ⟶ C → G : B ⟶ C
12 eqimss2 ⊢ ran ⁡ F = B → B ⊆ ran ⁡ F
13 funfocofob ⊢ Fun ⁡ F ∧ G : B ⟶ C ∧ B ⊆ ran ⁡ F → G ∘ F : F -1 B ⟶ onto C ↔ G : B ⟶ onto C
14 10 11 12 13 syl3an ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → G ∘ F : F -1 B ⟶ onto C ↔ G : B ⟶ onto C
15 9 14 bitrd ⊢ F Fn A ∧ G : B ⟶ C ∧ ran ⁡ F = B → G ∘ F : A ⟶ onto C ↔ G : B ⟶ onto C