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