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 𝐸 = ( ExtStrCat ‘ 𝑈 )
funcestrcsetc.s 𝑆 = ( SetCat ‘ 𝑈 )
funcestrcsetc.b 𝐵 = ( Base ‘ 𝐸 )
funcestrcsetc.c 𝐶 = ( Base ‘ 𝑆 )
funcestrcsetc.u ( 𝜑𝑈 ∈ WUni )
funcestrcsetc.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
funcestrcsetc.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
Assertion fullestrcsetc ( 𝜑𝐹 ( 𝐸 Full 𝑆 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e 𝐸 = ( ExtStrCat ‘ 𝑈 )
2 funcestrcsetc.s 𝑆 = ( SetCat ‘ 𝑈 )
3 funcestrcsetc.b 𝐵 = ( Base ‘ 𝐸 )
4 funcestrcsetc.c 𝐶 = ( Base ‘ 𝑆 )
5 funcestrcsetc.u ( 𝜑𝑈 ∈ WUni )
6 funcestrcsetc.f ( 𝜑𝐹 = ( 𝑥𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7 funcestrcsetc.g ( 𝜑𝐺 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
8 1 2 3 4 5 6 7 funcestrcsetc ( 𝜑𝐹 ( 𝐸 Func 𝑆 ) 𝐺 )
9 1 2 3 4 5 6 7 funcestrcsetclem8 ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ⟶ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) )
10 5 adantr ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑈 ∈ WUni )
11 eqid ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
12 1 2 3 4 5 6 funcestrcsetclem2 ( ( 𝜑𝑎𝐵 ) → ( 𝐹𝑎 ) ∈ 𝑈 )
13 12 adantrr ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐹𝑎 ) ∈ 𝑈 )
14 1 2 3 4 5 6 funcestrcsetclem2 ( ( 𝜑𝑏𝐵 ) → ( 𝐹𝑏 ) ∈ 𝑈 )
15 14 adantrl ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐹𝑏 ) ∈ 𝑈 )
16 2 10 11 13 15 elsetchom ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ∈ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) ↔ : ( 𝐹𝑎 ) ⟶ ( 𝐹𝑏 ) ) )
17 1 2 3 4 5 6 funcestrcsetclem1 ( ( 𝜑𝑎𝐵 ) → ( 𝐹𝑎 ) = ( Base ‘ 𝑎 ) )
18 17 adantrr ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐹𝑎 ) = ( Base ‘ 𝑎 ) )
19 1 2 3 4 5 6 funcestrcsetclem1 ( ( 𝜑𝑏𝐵 ) → ( 𝐹𝑏 ) = ( Base ‘ 𝑏 ) )
20 19 adantrl ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝐹𝑏 ) = ( Base ‘ 𝑏 ) )
21 18 20 feq23d ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( : ( 𝐹𝑎 ) ⟶ ( 𝐹𝑏 ) ↔ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
22 16 21 bitrd ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ∈ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) ↔ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
23 fvex ( Base ‘ 𝑏 ) ∈ V
24 fvex ( Base ‘ 𝑎 ) ∈ V
25 23 24 pm3.2i ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V )
26 elmapg ( ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V ) → ( ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ↔ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
27 25 26 mp1i ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ↔ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
28 27 biimpar ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
29 equequ2 ( 𝑘 = → ( = 𝑘 = ) )
30 29 adantl ( ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) ∧ 𝑘 = ) → ( = 𝑘 = ) )
31 eqidd ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → = )
32 28 30 31 rspcedvd ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = 𝑘 )
33 eqid ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
34 eqid ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
35 1 2 3 4 5 6 7 33 34 funcestrcsetclem6 ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
36 35 3expa ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
37 36 eqeq2d ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) → ( = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ = 𝑘 ) )
38 37 rexbidva ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = 𝑘 ) )
39 38 adantr ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ( ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = 𝑘 ) )
40 32 39 mpbird ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) )
41 eqid ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
42 1 5 estrcbas ( 𝜑𝑈 = ( Base ‘ 𝐸 ) )
43 3 42 eqtr4id ( 𝜑𝐵 = 𝑈 )
44 43 eleq2d ( 𝜑 → ( 𝑎𝐵𝑎𝑈 ) )
45 44 biimpcd ( 𝑎𝐵 → ( 𝜑𝑎𝑈 ) )
46 45 adantr ( ( 𝑎𝐵𝑏𝐵 ) → ( 𝜑𝑎𝑈 ) )
47 46 impcom ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑎𝑈 )
48 43 eleq2d ( 𝜑 → ( 𝑏𝐵𝑏𝑈 ) )
49 48 biimpcd ( 𝑏𝐵 → ( 𝜑𝑏𝑈 ) )
50 49 adantl ( ( 𝑎𝐵𝑏𝐵 ) → ( 𝜑𝑏𝑈 ) )
51 50 impcom ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → 𝑏𝑈 )
52 1 10 41 47 51 33 34 estrchom ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
53 52 rexeqdv ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
54 53 adantr ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ( ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
55 40 54 mpbird ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) )
56 55 ex ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) → ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
57 22 56 sylbid ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( ∈ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) → ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
58 57 ralrimiv ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ∀ ∈ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) )
59 dffo3 ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –onto→ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) ↔ ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) ⟶ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) ∧ ∀ ∈ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
60 9 58 59 sylanbrc ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –onto→ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) )
61 60 ralrimivva ( 𝜑 → ∀ 𝑎𝐵𝑏𝐵 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –onto→ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) )
62 3 11 41 isfull2 ( 𝐹 ( 𝐸 Full 𝑆 ) 𝐺 ↔ ( 𝐹 ( 𝐸 Func 𝑆 ) 𝐺 ∧ ∀ 𝑎𝐵𝑏𝐵 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝐸 ) 𝑏 ) –onto→ ( ( 𝐹𝑎 ) ( Hom ‘ 𝑆 ) ( 𝐹𝑏 ) ) ) )
63 8 61 62 sylanbrc ( 𝜑𝐹 ( 𝐸 Full 𝑆 ) 𝐺 )