Metamath Proof Explorer

Theorem fullestrcsetc

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 full. (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 fullestrcsetc ⊢ φ → F E Full 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 ⁡ S = Hom ⁡ S
12 1 2 3 4 5 6 funcestrcsetclem2 ⊢ φ ∧ a ∈ B → F ⁡ a ∈ U
13 12 adantrr ⊢ φ ∧ a ∈ B ∧ b ∈ B → F ⁡ a ∈ U
14 1 2 3 4 5 6 funcestrcsetclem2 ⊢ φ ∧ b ∈ B → F ⁡ b ∈ U
15 14 adantrl ⊢ φ ∧ a ∈ B ∧ b ∈ B → F ⁡ b ∈ U
16 2 10 11 13 15 elsetchom ⊢ φ ∧ a ∈ B ∧ b ∈ B → h ∈ F ⁡ a Hom ⁡ S F ⁡ b ↔ h : F ⁡ a ⟶ F ⁡ b
17 1 2 3 4 5 6 funcestrcsetclem1 ⊢ φ ∧ a ∈ B → F ⁡ a = Base a
18 17 adantrr ⊢ φ ∧ a ∈ B ∧ b ∈ B → F ⁡ a = Base a
19 1 2 3 4 5 6 funcestrcsetclem1 ⊢ φ ∧ b ∈ B → F ⁡ b = Base b
20 19 adantrl ⊢ φ ∧ a ∈ B ∧ b ∈ B → F ⁡ b = Base b
21 18 20 feq23d ⊢ φ ∧ a ∈ B ∧ b ∈ B → h : F ⁡ a ⟶ F ⁡ b ↔ h : Base a ⟶ Base b
22 16 21 bitrd ⊢ φ ∧ a ∈ B ∧ b ∈ B → h ∈ F ⁡ a Hom ⁡ S F ⁡ b ↔ h : Base a ⟶ Base b
23 fvex ⊢ Base b ∈ V
24 fvex ⊢ Base a ∈ V
25 23 24 pm3.2i ⊢ Base b ∈ V ∧ Base a ∈ V
26 elmapg ⊢ Base b ∈ V ∧ Base a ∈ V → h ∈ Base b Base a ↔ h : Base a ⟶ Base b
27 25 26 mp1i ⊢ φ ∧ a ∈ B ∧ b ∈ B → h ∈ Base b Base a ↔ h : Base a ⟶ Base b
28 27 biimpar ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b → h ∈ Base b Base a
29 equequ2 ⊢ k = h → h = k ↔ h = h
30 29 adantl ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b ∧ k = h → h = k ↔ h = h
31 eqidd ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b → h = h
32 28 30 31 rspcedvd ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b → ∃ k ∈ Base b Base a h = k
33 eqid ⊢ Base a = Base a
34 eqid ⊢ Base b = Base b
35 1 2 3 4 5 6 7 33 34 funcestrcsetclem6 ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ k ∈ Base b Base a → a G b ⁡ k = k
36 35 3expa ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ k ∈ Base b Base a → a G b ⁡ k = k
37 36 eqeq2d ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ k ∈ Base b Base a → h = a G b ⁡ k ↔ h = k
38 37 rexbidva ⊢ φ ∧ a ∈ B ∧ b ∈ B → ∃ k ∈ Base b Base a h = a G b ⁡ k ↔ ∃ k ∈ Base b Base a h = k
39 38 adantr ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b → ∃ k ∈ Base b Base a h = a G b ⁡ k ↔ ∃ k ∈ Base b Base a h = k
40 32 39 mpbird ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b → ∃ k ∈ Base b Base a h = a G b ⁡ k
41 eqid ⊢ Hom ⁡ E = Hom ⁡ E
42 1 5 estrcbas ⊢ φ → U = Base E
43 3 42 eqtr4id ⊢ φ → B = U
44 43 eleq2d ⊢ φ → a ∈ B ↔ a ∈ U
45 44 biimpcd ⊢ a ∈ B → φ → a ∈ U
46 45 adantr ⊢ a ∈ B ∧ b ∈ B → φ → a ∈ U
47 46 impcom ⊢ φ ∧ a ∈ B ∧ b ∈ B → a ∈ U
48 43 eleq2d ⊢ φ → b ∈ B ↔ b ∈ U
49 48 biimpcd ⊢ b ∈ B → φ → b ∈ U
50 49 adantl ⊢ a ∈ B ∧ b ∈ B → φ → b ∈ U
51 50 impcom ⊢ φ ∧ a ∈ B ∧ b ∈ B → b ∈ U
52 1 10 41 47 51 33 34 estrchom ⊢ φ ∧ a ∈ B ∧ b ∈ B → a Hom ⁡ E b = Base b Base a
53 52 rexeqdv ⊢ φ ∧ a ∈ B ∧ b ∈ B → ∃ k ∈ a Hom ⁡ E b h = a G b ⁡ k ↔ ∃ k ∈ Base b Base a h = a G b ⁡ k
54 53 adantr ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b → ∃ k ∈ a Hom ⁡ E b h = a G b ⁡ k ↔ ∃ k ∈ Base b Base a h = a G b ⁡ k
55 40 54 mpbird ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ h : Base a ⟶ Base b → ∃ k ∈ a Hom ⁡ E b h = a G b ⁡ k
56 55 ex ⊢ φ ∧ a ∈ B ∧ b ∈ B → h : Base a ⟶ Base b → ∃ k ∈ a Hom ⁡ E b h = a G b ⁡ k
57 22 56 sylbid ⊢ φ ∧ a ∈ B ∧ b ∈ B → h ∈ F ⁡ a Hom ⁡ S F ⁡ b → ∃ k ∈ a Hom ⁡ E b h = a G b ⁡ k
58 57 ralrimiv ⊢ φ ∧ a ∈ B ∧ b ∈ B → ∀ h ∈ F ⁡ a Hom ⁡ S F ⁡ b ∃ k ∈ a Hom ⁡ E b h = a G b ⁡ k
59 dffo3 ⊢ a G b : a Hom ⁡ E b ⟶ onto F ⁡ a Hom ⁡ S F ⁡ b ↔ a G b : a Hom ⁡ E b ⟶ F ⁡ a Hom ⁡ S F ⁡ b ∧ ∀ h ∈ F ⁡ a Hom ⁡ S F ⁡ b ∃ k ∈ a Hom ⁡ E b h = a G b ⁡ k
60 9 58 59 sylanbrc ⊢ φ ∧ a ∈ B ∧ b ∈ B → a G b : a Hom ⁡ E b ⟶ onto F ⁡ a Hom ⁡ S F ⁡ b
61 60 ralrimivva ⊢ φ → ∀ a ∈ B ∀ b ∈ B a G b : a Hom ⁡ E b ⟶ onto F ⁡ a Hom ⁡ S F ⁡ b
62 3 11 41 isfull2 ⊢ F E Full S G ↔ F E Func S G ∧ ∀ a ∈ B ∀ b ∈ B a G b : a Hom ⁡ E b ⟶ onto F ⁡ a Hom ⁡ S F ⁡ b
63 8 61 62 sylanbrc ⊢ φ → F E Full S G