Metamath Proof Explorer

Theorem ressffth

Description: The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in Adamek p. 49. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses ressffth.d ⊢ 𝐷 = ( 𝐶 ↾s 𝑆 )
ressffth.i ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
Assertion ressffth ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐼 ∈ ( ( 𝐷 Full 𝐶 ) ∩ ( 𝐷 Faith 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ressffth.d ⊢ 𝐷 = ( 𝐶 ↾s 𝑆 )
2 ressffth.i ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
3 relfunc ⊢ Rel ( 𝐷 Func 𝐷 )
4 resscat ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾s 𝑆 ) ∈ Cat )
5 1 4 eqeltrid ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐷 ∈ Cat )
6 2 idfucl ⊢ ( 𝐷 ∈ Cat → 𝐼 ∈ ( 𝐷 Func 𝐷 ) )
7 5 6 syl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐼 ∈ ( 𝐷 Func 𝐷 ) )
8 1st2nd ⊢ ( ( Rel ( 𝐷 Func 𝐷 ) ∧ 𝐼 ∈ ( 𝐷 Func 𝐷 ) ) → 𝐼 = ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ )
9 3 7 8 sylancr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐼 = ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ )
10 eqidd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐷 ) )
11 eqidd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( compf ‘ 𝐷 ) = ( compf ‘ 𝐷 ) )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 12 ressinbas ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) )
14 13 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) )
15 1 14 eqtrid ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐷 = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) )
16 15 fveq2d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) )
17 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
18 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐶 ∈ Cat )
19 inss2 ⊢ ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐶 )
20 19 a1i ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐶 ) )
21 eqid ⊢ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) )
22 eqid ⊢ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) = ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) )
23 12 17 18 20 21 22 fullresc ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( ( Homf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) ∧ ( compf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) ) )
24 23 simpld ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( Homf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) )
25 16 24 eqtrd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) )
26 15 fveq2d ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( compf ‘ 𝐷 ) = ( compf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) )
27 23 simprd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( compf ‘ ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) = ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) )
28 26 27 eqtrd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( compf ‘ 𝐷 ) = ( compf ‘ ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) )
29 1 ovexi ⊢ 𝐷 ∈ V
30 29 a1i ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐷 ∈ V )
31 ovexd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ∈ V )
32 10 11 25 28 30 30 30 31 funcpropd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐷 Func 𝐷 ) = ( 𝐷 Func ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) )
33 12 17 18 20 fullsubc ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ∈ ( Subcat ‘ 𝐶 ) )
34 funcres2 ⊢ ( ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ∈ ( Subcat ‘ 𝐶 ) → ( 𝐷 Func ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) ⊆ ( 𝐷 Func 𝐶 ) )
35 33 34 syl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐷 Func ( 𝐶 ↾cat ( ( Homf ‘ 𝐶 ) ↾ ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) × ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) ) ) ) ⊆ ( 𝐷 Func 𝐶 ) )
36 32 35 eqsstrd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 𝐷 Func 𝐷 ) ⊆ ( 𝐷 Func 𝐶 ) )
37 36 7 sseldd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐼 ∈ ( 𝐷 Func 𝐶 ) )
38 9 37 eqeltrrd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( 𝐷 Func 𝐶 ) )
39 df-br ⊢ ( ( 1st ‘ 𝐼 ) ( 𝐷 Func 𝐶 ) ( 2nd ‘ 𝐼 ) ↔ ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( 𝐷 Func 𝐶 ) )
40 38 39 sylibr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 1st ‘ 𝐼 ) ( 𝐷 Func 𝐶 ) ( 2nd ‘ 𝐼 ) )
41 f1oi ⊢ ( I ↾ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1-onto→ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 )
42 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
43 5 adantr ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐷 ∈ Cat )
44 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
45 simprl ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐷 ) )
46 simprr ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
47 2 42 43 44 45 46 idfu2nd ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
48 eqidd ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
49 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
50 1 49 resshom ⊢ ( 𝑆 ∈ 𝑉 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐷 ) )
51 50 ad2antlr ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐷 ) )
52 2 42 43 45 idfu1 ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) = 𝑥 )
53 2 42 43 46 idfu1 ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) = 𝑦 )
54 51 52 53 oveq123d ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
55 47 48 54 f1oeq123d ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) ↔ ( I ↾ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1-onto→ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
56 41 55 mpbiri ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) )
57 56 ralrimivva ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) )
58 42 44 49 isffth2 ⊢ ( ( 1st ‘ 𝐼 ) ( ( 𝐷 Full 𝐶 ) ∩ ( 𝐷 Faith 𝐶 ) ) ( 2nd ‘ 𝐼 ) ↔ ( ( 1st ‘ 𝐼 ) ( 𝐷 Func 𝐶 ) ( 2nd ‘ 𝐼 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 2nd ‘ 𝐼 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) –1-1-onto→ ( ( ( 1st ‘ 𝐼 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1st ‘ 𝐼 ) ‘ 𝑦 ) ) ) )
59 40 57 58 sylanbrc ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ( 1st ‘ 𝐼 ) ( ( 𝐷 Full 𝐶 ) ∩ ( 𝐷 Faith 𝐶 ) ) ( 2nd ‘ 𝐼 ) )
60 df-br ⊢ ( ( 1st ‘ 𝐼 ) ( ( 𝐷 Full 𝐶 ) ∩ ( 𝐷 Faith 𝐶 ) ) ( 2nd ‘ 𝐼 ) ↔ ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( ( 𝐷 Full 𝐶 ) ∩ ( 𝐷 Faith 𝐶 ) ) )
61 59 60 sylib ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → ⟨ ( 1st ‘ 𝐼 ) , ( 2nd ‘ 𝐼 ) ⟩ ∈ ( ( 𝐷 Full 𝐶 ) ∩ ( 𝐷 Faith 𝐶 ) ) )
62 9 61 eqeltrd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉 ) → 𝐼 ∈ ( ( 𝐷 Full 𝐶 ) ∩ ( 𝐷 Faith 𝐶 ) ) )