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

Metamath Proof Explorer

Theorem fcofo

Description: An application is surjective if a section exists. Proposition 8 of BourbakiEns p. E.II.18. (Contributed by FL, 17-Nov-2011) (Proof shortened by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion fcofo ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) → 𝐹 : 𝐴 –onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 ffvelcdm ⊢ ( ( 𝑆 : 𝐵 ⟶ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 ‘ 𝑦 ) ∈ 𝐴 )
3 2 3ad2antl2 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 ‘ 𝑦 ) ∈ 𝐴 )
4 simpl3 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) )
5 4 fveq1d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑆 ) ‘ 𝑦 ) = ( ( I ↾ 𝐵 ) ‘ 𝑦 ) )
6 fvco3 ⊢ ( ( 𝑆 : 𝐵 ⟶ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑆 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑆 ‘ 𝑦 ) ) )
7 6 3ad2antl2 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝑆 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑆 ‘ 𝑦 ) ) )
8 fvresi ⊢ ( 𝑦 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
9 8 adantl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
10 5 7 9 3eqtr3rd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 = ( 𝐹 ‘ ( 𝑆 ‘ 𝑦 ) ) )
11 fveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑆 ‘ 𝑦 ) ) )
12 11 rspceeqv ⊢ ( ( ( 𝑆 ‘ 𝑦 ) ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ ( 𝑆 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
13 3 10 12 syl2anc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
14 13 ralrimiva ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) )
15 dffo3 ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
16 1 14 15 sylanbrc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑆 : 𝐵 ⟶ 𝐴 ∧ ( 𝐹 ∘ 𝑆 ) = ( I ↾ 𝐵 ) ) → 𝐹 : 𝐴 –onto→ 𝐵 )