Theorem embedsetcestrc

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 is an embedding. According to definition 3.27 (1) of Adamek p. 34, a functor "F is called an embedding provided that F is injective on morphisms", or according to remark 3.28 (1) in Adamek p. 34, "a functor is an embedding if and only if it is faithful and injective on objects". (Contributed by AV, 31-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 ‘ 𝑈 )
	embedsetcestrc.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
Assertion	embedsetcestrc	⊢ ( 𝜑 → ( 𝐹 ( 𝑆 Faith 𝐸 ) 𝐺 ∧ 𝐹 : 𝐶 –1-1→ 𝐵 ) )

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		embedsetcestrc.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
9	1 2 3 4 5 6 7	fthsetcestrc	⊢ ( 𝜑 → 𝐹 ( 𝑆 Faith 𝐸 ) 𝐺 )
10	1 2 3 4 5 7 8	embedsetcestrclem	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1→ 𝐵 )
11	9 10	jca	⊢ ( 𝜑 → ( 𝐹 ( 𝑆 Faith 𝐸 ) 𝐺 ∧ 𝐹 : 𝐶 –1-1→ 𝐵 ) )