Metamath Proof Explorer

Theorem fthsetcestrc

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 faithful. (Contributed by AV, 31-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ S = SetCat ⁡ U
funcsetcestrc.c ⊢ C = Base S
funcsetcestrc.f ⊢ φ → F = x ∈ C ⟼ Base ndx x
funcsetcestrc.u ⊢ φ → U ∈ WUni
funcsetcestrc.o ⊢ φ → ω ∈ U
funcsetcestrc.g ⊢ φ → G = x ∈ C , y ∈ C ⟼ I ↾ y x
funcsetcestrc.e ⊢ E = ExtStrCat ⁡ U
Assertion fthsetcestrc ⊢ φ → F S Faith E G

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ S = SetCat ⁡ U
2 funcsetcestrc.c ⊢ C = Base S
3 funcsetcestrc.f ⊢ φ → F = x ∈ C ⟼ Base ndx x
4 funcsetcestrc.u ⊢ φ → U ∈ WUni
5 funcsetcestrc.o ⊢ φ → ω ∈ U
6 funcsetcestrc.g ⊢ φ → G = x ∈ C , y ∈ C ⟼ I ↾ y x
7 funcsetcestrc.e ⊢ E = ExtStrCat ⁡ U
8 1 2 3 4 5 6 7 funcsetcestrc ⊢ φ → F S Func E G
9 1 2 3 4 5 6 7 funcsetcestrclem8 ⊢ φ ∧ a ∈ C ∧ b ∈ C → a G b : a Hom ⁡ S b ⟶ F ⁡ a Hom ⁡ E F ⁡ b
10 4 adantr ⊢ φ ∧ a ∈ C ∧ b ∈ C → U ∈ WUni
11 eqid ⊢ Hom ⁡ S = Hom ⁡ S
12 1 4 setcbas ⊢ φ → U = Base S
13 2 12 eqtr4id ⊢ φ → C = U
14 13 eleq2d ⊢ φ → a ∈ C ↔ a ∈ U
15 14 biimpcd ⊢ a ∈ C → φ → a ∈ U
16 15 adantr ⊢ a ∈ C ∧ b ∈ C → φ → a ∈ U
17 16 impcom ⊢ φ ∧ a ∈ C ∧ b ∈ C → a ∈ U
18 13 eleq2d ⊢ φ → b ∈ C ↔ b ∈ U
19 18 biimpcd ⊢ b ∈ C → φ → b ∈ U
20 19 adantl ⊢ a ∈ C ∧ b ∈ C → φ → b ∈ U
21 20 impcom ⊢ φ ∧ a ∈ C ∧ b ∈ C → b ∈ U
22 1 10 11 17 21 setchom ⊢ φ ∧ a ∈ C ∧ b ∈ C → a Hom ⁡ S b = b a
23 22 eleq2d ⊢ φ ∧ a ∈ C ∧ b ∈ C → h ∈ a Hom ⁡ S b ↔ h ∈ b a
24 1 2 3 4 5 6 funcsetcestrclem6 ⊢ φ ∧ a ∈ C ∧ b ∈ C ∧ h ∈ b a → a G b ⁡ h = h
25 24 3expia ⊢ φ ∧ a ∈ C ∧ b ∈ C → h ∈ b a → a G b ⁡ h = h
26 23 25 sylbid ⊢ φ ∧ a ∈ C ∧ b ∈ C → h ∈ a Hom ⁡ S b → a G b ⁡ h = h
27 26 com12 ⊢ h ∈ a Hom ⁡ S b → φ ∧ a ∈ C ∧ b ∈ C → a G b ⁡ h = h
28 27 adantr ⊢ h ∈ a Hom ⁡ S b ∧ k ∈ a Hom ⁡ S b → φ ∧ a ∈ C ∧ b ∈ C → a G b ⁡ h = h
29 28 impcom ⊢ φ ∧ a ∈ C ∧ b ∈ C ∧ h ∈ a Hom ⁡ S b ∧ k ∈ a Hom ⁡ S b → a G b ⁡ h = h
30 22 eleq2d ⊢ φ ∧ a ∈ C ∧ b ∈ C → k ∈ a Hom ⁡ S b ↔ k ∈ b a
31 1 2 3 4 5 6 funcsetcestrclem6 ⊢ φ ∧ a ∈ C ∧ b ∈ C ∧ k ∈ b a → a G b ⁡ k = k
32 31 3expia ⊢ φ ∧ a ∈ C ∧ b ∈ C → k ∈ b a → a G b ⁡ k = k
33 30 32 sylbid ⊢ φ ∧ a ∈ C ∧ b ∈ C → k ∈ a Hom ⁡ S b → a G b ⁡ k = k
34 33 com12 ⊢ k ∈ a Hom ⁡ S b → φ ∧ a ∈ C ∧ b ∈ C → a G b ⁡ k = k
35 34 adantl ⊢ h ∈ a Hom ⁡ S b ∧ k ∈ a Hom ⁡ S b → φ ∧ a ∈ C ∧ b ∈ C → a G b ⁡ k = k
36 35 impcom ⊢ φ ∧ a ∈ C ∧ b ∈ C ∧ h ∈ a Hom ⁡ S b ∧ k ∈ a Hom ⁡ S b → a G b ⁡ k = k
37 29 36 eqeq12d ⊢ φ ∧ a ∈ C ∧ b ∈ C ∧ h ∈ a Hom ⁡ S b ∧ k ∈ a Hom ⁡ S b → a G b ⁡ h = a G b ⁡ k ↔ h = k
38 37 biimpd ⊢ φ ∧ a ∈ C ∧ b ∈ C ∧ h ∈ a Hom ⁡ S b ∧ k ∈ a Hom ⁡ S b → a G b ⁡ h = a G b ⁡ k → h = k
39 38 ralrimivva ⊢ φ ∧ a ∈ C ∧ b ∈ C → ∀ h ∈ a Hom ⁡ S b ∀ k ∈ a Hom ⁡ S b a G b ⁡ h = a G b ⁡ k → h = k
40 dff13 ⊢ a G b : a Hom ⁡ S b ⟶ 1-1 F ⁡ a Hom ⁡ E F ⁡ b ↔ a G b : a Hom ⁡ S b ⟶ F ⁡ a Hom ⁡ E F ⁡ b ∧ ∀ h ∈ a Hom ⁡ S b ∀ k ∈ a Hom ⁡ S b a G b ⁡ h = a G b ⁡ k → h = k
41 9 39 40 sylanbrc ⊢ φ ∧ a ∈ C ∧ b ∈ C → a G b : a Hom ⁡ S b ⟶ 1-1 F ⁡ a Hom ⁡ E F ⁡ b
42 41 ralrimivva ⊢ φ → ∀ a ∈ C ∀ b ∈ C a G b : a Hom ⁡ S b ⟶ 1-1 F ⁡ a Hom ⁡ E F ⁡ b
43 eqid ⊢ Hom ⁡ E = Hom ⁡ E
44 2 11 43 isfth2 ⊢ F S Faith E G ↔ F S Func E G ∧ ∀ a ∈ C ∀ b ∈ C a G b : a Hom ⁡ S b ⟶ 1-1 F ⁡ a Hom ⁡ E F ⁡ b
45 8 42 44 sylanbrc ⊢ φ → F S Faith E G