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

Metamath Proof Explorer

Theorem foco2

Description: If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion foco2 ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) → 𝐹 : 𝐵 –onto→ 𝐶 )

Proof

Step Hyp Ref Expression
1 foelrn ⊢ ( ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑧 ∈ 𝐴 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) )
2 ffvelcdm ⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝐵 )
3 fvco3 ⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
4 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
5 4 rspceeqv ⊢ ( ( ( 𝐺 ‘ 𝑧 ) ∈ 𝐵 ∧ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
6 2 3 5 syl2anc ⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
7 eqeq1 ⊢ ( 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
8 7 rexbidv ⊢ ( 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ( ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐵 ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
9 6 8 syl5ibrcom ⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
10 9 rexlimdva ⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
11 1 10 syl5 ⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ( ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
12 11 impl ⊢ ( ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) )
13 12 ralrimiva ⊢ ( ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) → ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) )
14 13 anim2i ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ) → ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
15 3anass ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) ) )
16 dffo3 ⊢ ( 𝐹 : 𝐵 –onto→ 𝐶 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
17 14 15 16 3imtr4i ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ∧ ( 𝐹 ∘ 𝐺 ) : 𝐴 –onto→ 𝐶 ) → 𝐹 : 𝐵 –onto→ 𝐶 )