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

Metamath Proof Explorer

Theorem inclfusubc

Description: The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020)

Ref Expression
Hypotheses inclfusubc.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
inclfusubc.s ⊢ 𝑆 = ( 𝐶 ↾cat 𝐽 )
inclfusubc.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
inclfusubc.f ⊢ ( 𝜑 → 𝐹 = ( I ↾ 𝐵 ) )
inclfusubc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) )
Assertion inclfusubc ( 𝜑 → 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 inclfusubc.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2 inclfusubc.s ⊢ 𝑆 = ( 𝐶 ↾cat 𝐽 )
3 inclfusubc.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 inclfusubc.f ⊢ ( 𝜑 → 𝐹 = ( I ↾ 𝐵 ) )
5 inclfusubc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) )
6 fthfunc ⊢ ( 𝑆 Faith 𝐶 ) ⊆ ( 𝑆 Func 𝐶 )
7 eqid ⊢ ( idfunc ‘ 𝑆 ) = ( idfunc ‘ 𝑆 )
8 2 7 rescfth ⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Faith 𝐶 ) )
9 1 8 syl ⊢ ( 𝜑 → ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Faith 𝐶 ) )
10 6 9 sselid ⊢ ( 𝜑 → ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Func 𝐶 ) )
11 df-br ⊢ ( 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 Func 𝐶 ) )
12 4 5 opeq12d ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )
13 2 7 3 idfusubc ⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( idfunc ‘ 𝑆 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )
14 1 13 syl ⊢ ( 𝜑 → ( idfunc ‘ 𝑆 ) = ⟨ ( I ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 𝐽 𝑦 ) ) ) ⟩ )
15 12 14 eqtr4d ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ( idfunc ‘ 𝑆 ) )
16 15 eleq1d ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑆 Func 𝐶 ) ↔ ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Func 𝐶 ) ) )
17 11 16 bitrid ⊢ ( 𝜑 → ( 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 ↔ ( idfunc ‘ 𝑆 ) ∈ ( 𝑆 Func 𝐶 ) ) )
18 10 17 mpbird ⊢ ( 𝜑 → 𝐹 ( 𝑆 Func 𝐶 ) 𝐺 )