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

Metamath Proof Explorer

Theorem fcof1

Description: An application is injective if a retraction exists. Proposition 8 of BourbakiEns p. E.II.18. (Contributed by FL, 11-Nov-2011) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion fcof1 ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 simprr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
3 2 fveq2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑅 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑅 ‘ ( 𝐹 ‘ 𝑦 ) ) )
4 simpll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
5 simprll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 ∈ 𝐴 )
6 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝑅 ‘ ( 𝐹 ‘ 𝑥 ) ) )
7 4 5 6 syl2anc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝑅 ‘ ( 𝐹 ‘ 𝑥 ) ) )
8 simprlr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 ∈ 𝐴 )
9 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑦 ) = ( 𝑅 ‘ ( 𝐹 ‘ 𝑦 ) ) )
10 4 8 9 syl2anc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑦 ) = ( 𝑅 ‘ ( 𝐹 ‘ 𝑦 ) ) )
11 3 7 10 3eqtr4d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑦 ) )
12 simplr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
13 12 fveq1d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) )
14 12 fveq1d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑅 ∘ 𝐹 ) ‘ 𝑦 ) = ( ( I ↾ 𝐴 ) ‘ 𝑦 ) )
15 11 13 14 3eqtr3d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑦 ) )
16 fvresi ⊢ ( 𝑥 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
17 5 16 syl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
18 fvresi ⊢ ( 𝑦 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑦 ) = 𝑦 )
19 8 18 syl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( I ↾ 𝐴 ) ‘ 𝑦 ) = 𝑦 )
20 15 17 19 3eqtr3d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 )
21 20 expr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
22 21 ralrimivva ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
23 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
24 1 22 23 sylanbrc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝑅 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) → 𝐹 : 𝐴 –1-1→ 𝐵 )