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 𝑆 ) 𝐺 )