This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fullsetcestrc

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 full. (Contributed by AV, 1-Apr-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
Assertion fullsetcestrc ( 𝜑 → 𝐹 ( 𝑆 Full 𝐸 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2 funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
4 funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
6 funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
7 funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
8 1 2 3 4 5 6 7 funcsetcestrc ⊢ ( 𝜑 → 𝐹 ( 𝑆 Func 𝐸 ) 𝐺 )
9 1 2 3 4 5 6 7 funcsetcestrclem8 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) )
10 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑈 ∈ WUni )
11 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
12 1 2 3 4 5 funcsetcestrclem2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝑈 )
13 12 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝑈 )
14 1 2 3 4 5 funcsetcestrclem2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑈 )
15 14 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝑈 )
16 eqid ⊢ ( Base ‘ ( 𝐹 ‘ 𝑎 ) ) = ( Base ‘ ( 𝐹 ‘ 𝑎 ) )
17 eqid ⊢ ( Base ‘ ( 𝐹 ‘ 𝑏 ) ) = ( Base ‘ ( 𝐹 ‘ 𝑏 ) )
18 7 10 11 13 15 16 17 elestrchom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ ∈ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ↔ ℎ : ( Base ‘ ( 𝐹 ‘ 𝑎 ) ) ⟶ ( Base ‘ ( 𝐹 ‘ 𝑏 ) ) ) )
19 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑎 ) = { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ } )
20 19 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑎 ) = { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ } )
21 20 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑎 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ } ) )
22 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ }
23 22 1strbas ⊢ ( 𝑎 ∈ 𝐶 → 𝑎 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ } ) )
24 23 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑎 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ } ) )
25 21 24 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑎 ) ) = 𝑎 )
26 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑏 ) = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } )
27 26 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑏 ) = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } )
28 27 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑏 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
29 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ }
30 29 1strbas ⊢ ( 𝑏 ∈ 𝐶 → 𝑏 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
31 30 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑏 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
32 28 31 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑏 ) ) = 𝑏 )
33 25 32 feq23d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ : ( Base ‘ ( 𝐹 ‘ 𝑎 ) ) ⟶ ( Base ‘ ( 𝐹 ‘ 𝑏 ) ) ↔ ℎ : 𝑎 ⟶ 𝑏 ) )
34 simpr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) )
35 34 ancomd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑏 ∈ 𝐶 ∧ 𝑎 ∈ 𝐶 ) )
36 elmapg ⊢ ( ( 𝑏 ∈ 𝐶 ∧ 𝑎 ∈ 𝐶 ) → ( ℎ ∈ ( 𝑏 ↑m 𝑎 ) ↔ ℎ : 𝑎 ⟶ 𝑏 ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ ∈ ( 𝑏 ↑m 𝑎 ) ↔ ℎ : 𝑎 ⟶ 𝑏 ) )
38 37 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) → ℎ ∈ ( 𝑏 ↑m 𝑎 ) )
39 equequ2 ⊢ ( 𝑘 = ℎ → ( ℎ = 𝑘 ↔ ℎ = ℎ ) )
40 39 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) ∧ 𝑘 = ℎ ) → ( ℎ = 𝑘 ↔ ℎ = ℎ ) )
41 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) → ℎ = ℎ )
42 38 40 41 rspcedvd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) → ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = 𝑘 )
43 1 2 3 4 5 6 funcsetcestrclem6 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
44 43 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ) → ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) = 𝑘 )
45 44 eqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ) → ( ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ℎ = 𝑘 ) )
46 45 rexbidva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = 𝑘 ) )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) → ( ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = 𝑘 ) )
48 42 47 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) → ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) )
49 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
50 1 4 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
51 2 50 eqtr4id ⊢ ( 𝜑 → 𝐶 = 𝑈 )
52 51 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐶 ↔ 𝑎 ∈ 𝑈 ) )
53 52 biimpcd ⊢ ( 𝑎 ∈ 𝐶 → ( 𝜑 → 𝑎 ∈ 𝑈 ) )
54 53 adantr ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝜑 → 𝑎 ∈ 𝑈 ) )
55 54 impcom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑎 ∈ 𝑈 )
56 51 eleq2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐶 ↔ 𝑏 ∈ 𝑈 ) )
57 56 biimpcd ⊢ ( 𝑏 ∈ 𝐶 → ( 𝜑 → 𝑏 ∈ 𝑈 ) )
58 57 adantl ⊢ ( ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) → ( 𝜑 → 𝑏 ∈ 𝑈 ) )
59 58 impcom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑏 ∈ 𝑈 )
60 1 10 49 55 59 setchom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) = ( 𝑏 ↑m 𝑎 ) )
61 60 rexeqdv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) → ( ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( 𝑏 ↑m 𝑎 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
63 48 62 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) ∧ ℎ : 𝑎 ⟶ 𝑏 ) → ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) )
64 63 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ : 𝑎 ⟶ 𝑏 → ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
65 33 64 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ : ( Base ‘ ( 𝐹 ‘ 𝑎 ) ) ⟶ ( Base ‘ ( 𝐹 ‘ 𝑏 ) ) → ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
66 18 65 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ℎ ∈ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) → ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
67 66 ralrimiv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ∀ ℎ ∈ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) )
68 dffo3 ⊢ ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –onto→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ⟶ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ∧ ∀ ℎ ∈ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ∃ 𝑘 ∈ ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) ℎ = ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑘 ) ) )
69 9 67 68 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –onto→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) )
70 69 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –onto→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) )
71 2 11 49 isfull2 ⊢ ( 𝐹 ( 𝑆 Full 𝐸 ) 𝐺 ↔ ( 𝐹 ( 𝑆 Func 𝐸 ) 𝐺 ∧ ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( 𝑎 𝐺 𝑏 ) : ( 𝑎 ( Hom ‘ 𝑆 ) 𝑏 ) –onto→ ( ( 𝐹 ‘ 𝑎 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑏 ) ) ) )
72 8 70 71 sylanbrc ⊢ ( 𝜑 → 𝐹 ( 𝑆 Full 𝐸 ) 𝐺 )