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		ffvelrn	⊢ ( ( 𝑆 : 𝐵 ⟶ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 ‘ 𝑦 ) ∈ 𝐴 )
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→ 𝐵 )