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

Metamath Proof Explorer

Theorem idffth

Description: The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypothesis idffth.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
Assertion idffth ( 𝐶 ∈ Cat → 𝐼 ∈ ( ( 𝐶 Full 𝐶 ) ∩ ( 𝐶 Faith 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 idffth.i ⊢ 𝐼 = ( idfunc ‘ 𝐶 )
2 relfunc ⊢ Rel ( 𝐶 Func 𝐶 )
3 1 idfucl ⊢ ( 𝐶 ∈ Cat → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
4 1st2nd ⊢ ( ( Rel ( 𝐶 Func 𝐶 ) ∧ 𝐼 ∈ ( 𝐶 Func 𝐶 ) ) → 𝐼 = ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ )
5 2 3 4 sylancr ⊢ ( 𝐶 ∈ Cat → 𝐼 = ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ )
6 5 3 eqeltrrd ⊢ ( 𝐶 ∈ Cat → ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( 𝐶 Func 𝐶 ) )
7 df-br ⊢ ( ( 1st ‘ 𝐼 ) ( 𝐶 Func 𝐶 ) ( 2nd ‘ 𝐼 ) ↔ ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( 𝐶 Func 𝐶 ) )
8 6 7 sylibr ⊢ ( 𝐶 ∈ Cat → ( 1st ‘ 𝐼 ) ( 𝐶 Func 𝐶 ) ( 2nd ‘ 𝐼 ) )
9 f1oi ⊢ ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 )
10 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
12 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13 simprl ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
14 simprr ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
15 1 10 11 12 13 14 idfu2nd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
16 eqidd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
17 1 10 11 13 idfu1 ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) = 𝑥 )
18 1 10 11 14 idfu1 ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) = 𝑦 )
19 17 18 oveq12d ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
20 15 16 19 f1oeq123d ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) ↔ ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
21 9 20 mpbiri ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) )
22 21 ralrimivva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) )
23 10 12 12 isffth2 ⊢ ( ( 1st ‘ 𝐼 ) ( ( 𝐶 Full 𝐶 ) ∩ ( 𝐶 Faith 𝐶 ) ) ( 2nd ‘ 𝐼 ) ↔ ( ( 1st ‘ 𝐼 ) ( 𝐶 Func 𝐶 ) ( 2nd ‘ 𝐼 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) ) )
24 8 22 23 sylanbrc ⊢ ( 𝐶 ∈ Cat → ( 1st ‘ 𝐼 ) ( ( 𝐶 Full 𝐶 ) ∩ ( 𝐶 Faith 𝐶 ) ) ( 2nd ‘ 𝐼 ) )
25 df-br ⊢ ( ( 1st ‘ 𝐼 ) ( ( 𝐶 Full 𝐶 ) ∩ ( 𝐶 Faith 𝐶 ) ) ( 2nd ‘ 𝐼 ) ↔ ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( ( 𝐶 Full 𝐶 ) ∩ ( 𝐶 Faith 𝐶 ) ) )
26 24 25 sylib ⊢ ( 𝐶 ∈ Cat → ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( ( 𝐶 Full 𝐶 ) ∩ ( 𝐶 Faith 𝐶 ) ) )
27 5 26 eqeltrd ⊢ ( 𝐶 ∈ Cat → 𝐼 ∈ ( ( 𝐶 Full 𝐶 ) ∩ ( 𝐶 Faith 𝐶 ) ) )