This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
2 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
3 2 3ad2ant1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → dom 𝐹 = 𝐴 )
4 1 3 eqtr2id ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → 𝐴 = ( ◡ 𝐹 “ ran 𝐹 ) )
5 imaeq2 ⊢ ( ran 𝐹 = 𝐵 → ( ◡ 𝐹 “ ran 𝐹 ) = ( ◡ 𝐹 “ 𝐵 ) )
6 5 3ad2ant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → ( ◡ 𝐹 “ ran 𝐹 ) = ( ◡ 𝐹 “ 𝐵 ) )
7 4 6 eqtrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → 𝐴 = ( ◡ 𝐹 “ 𝐵 ) )
8 foeq2 ⊢ ( 𝐴 = ( ◡ 𝐹 “ 𝐵 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐶 ↔ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐵 ) –onto→ 𝐶 ) )
9 7 8 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐶 ↔ ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐵 ) –onto→ 𝐶 ) )
10 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
11 id ⊢ ( 𝐺 : 𝐵 ⟶ 𝐶 → 𝐺 : 𝐵 ⟶ 𝐶 )
12 eqimss2 ⊢ ( ran 𝐹 = 𝐵 → 𝐵 ⊆ ran 𝐹 )
13 funfocofob ⊢ ( ( Fun 𝐹 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ 𝐵 ⊆ ran 𝐹 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐵 ) –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐶 ) )
14 10 11 12 13 syl3an ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → ( ( 𝐺 ∘ 𝐹 ) : ( ◡ 𝐹 “ 𝐵 ) –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐶 ) )
15 9 14 bitrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ran 𝐹 = 𝐵 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐶 ) )