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 𝐶 ) ) )