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

Metamath Proof Explorer

Theorem funcsetcestrc

Description: The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
Assertion funcsetcestrc ( 𝜑 → 𝐹 ( 𝑆 Func 𝐸 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2 funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
4 funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
6 funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
7 funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
8 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
9 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
10 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
11 eqid ⊢ ( Id ‘ 𝑆 ) = ( Id ‘ 𝑆 )
12 eqid ⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
13 eqid ⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
14 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
15 1 setccat ⊢ ( 𝑈 ∈ WUni → 𝑆 ∈ Cat )
16 4 15 syl ⊢ ( 𝜑 → 𝑆 ∈ Cat )
17 7 estrccat ⊢ ( 𝑈 ∈ WUni → 𝐸 ∈ Cat )
18 4 17 syl ⊢ ( 𝜑 → 𝐸 ∈ Cat )
19 1 2 3 4 5 7 8 funcsetcestrclem3 ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ ( Base ‘ 𝐸 ) )
20 1 2 3 4 5 6 funcsetcestrclem4 ⊢ ( 𝜑 → 𝐺 Fn ( 𝐶 × 𝐶 ) )
21 1 2 3 4 5 6 7 funcsetcestrclem8 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) )
22 1 2 3 4 5 6 7 funcsetcestrclem7 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝑆 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) )
23 1 2 3 4 5 6 7 funcsetcestrclem9 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ∧ 𝑘 ∈ ( 𝑏 ( Hom ‘ 𝑆 ) 𝑐 ) ) ) → ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑘 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝑆 ) 𝑐 ) ℎ ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑘 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ ℎ ) ) )
24 2 8 9 10 11 12 13 14 16 18 19 20 21 22 23 isfuncd ⊢ ( 𝜑 → 𝐹 ( 𝑆 Func 𝐸 ) 𝐺 )