Metamath Proof Explorer

Theorem fthestrcsetc

Description: The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is faithful. (Contributed by AV, 2-Apr-2020)

Ref Expression
Hypotheses funcestrcsetc.e ⊢ E = ExtStrCat ⁡ U
funcestrcsetc.s ⊢ S = SetCat ⁡ U
funcestrcsetc.b ⊢ B = Base E
funcestrcsetc.c ⊢ C = Base S
funcestrcsetc.u ⊢ φ → U ∈ WUni
funcestrcsetc.f ⊢ φ → F = x ∈ B ⟼ Base x
funcestrcsetc.g ⊢ φ → G = x ∈ B , y ∈ B ⟼ I ↾ Base y Base x
Assertion fthestrcsetc ⊢ φ → F E Faith S G

Proof

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