Theorem equivestrcsetc

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 an equivalence. According to definition 3.33 (1) of Adamek p. 36, "A functor F : A -> B is called an equivalence provided that it is full, faithful, and isomorphism-dense in the sense that for any B-object B' there exists some A-object A' such that F(A') is isomorphic to B'.". Therefore, the category of sets and the category of extensible structures are equivalent, according to definition 3.33 (2) of Adamek p. 36, "Categories A and B are called equivalent provided that there is an equivalence from A to B.". (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 ‘ 𝑥 ) ) ) ) )
	equivestrcsetc.i	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
Assertion	equivestrcsetc	⊢ ( 𝜑 → ( 𝐹 ( 𝐸 Faith 𝑆 ) 𝐺 ∧ 𝐹 ( 𝐸 Full 𝑆 ) 𝐺 ∧ ∀ 𝑏 ∈ 𝐶 ∃ 𝑎 ∈ 𝐵 ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ 𝑎 ) ) )

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		equivestrcsetc.i	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
9	1 2 3 4 5 6 7	fthestrcsetc	⊢ ( 𝜑 → 𝐹 ( 𝐸 Faith 𝑆 ) 𝐺 )
10	1 2 3 4 5 6 7	fullestrcsetc	⊢ ( 𝜑 → 𝐹 ( 𝐸 Full 𝑆 ) 𝐺 )
11	2 5	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
12	4 11	eqtr4id	⊢ ( 𝜑 → 𝐶 = 𝑈 )
13	12	eleq2d	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐶 ↔ 𝑏 ∈ 𝑈 ) )
14		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ }
15	14 5 8	1strwunbndx	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ∈ 𝑈 )
16	15	ex	⊢ ( 𝜑 → ( 𝑏 ∈ 𝑈 → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ∈ 𝑈 ) )
17	13 16	sylbid	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐶 → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ∈ 𝑈 ) )
18	17	imp	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ∈ 𝑈 )
19	1 5	estrcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐸 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → 𝑈 = ( Base ‘ 𝐸 ) )
21	3 20	eqtr4id	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → 𝐵 = 𝑈 )
22	18 21	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ∈ 𝐵 )
23		fveq2	⊢ ( 𝑎 = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
24	23	f1oeq3d	⊢ ( 𝑎 = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } → ( 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ 𝑎 ) ↔ 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) ) )
25	24	exbidv	⊢ ( 𝑎 = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } → ( ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ 𝑎 ) ↔ ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) ) )
26	25	adantl	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑎 = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) → ( ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ 𝑎 ) ↔ ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) ) )
27		f1oi	⊢ ( I ↾ 𝑏 ) : 𝑏 –1-1-onto→ 𝑏
28	1 2 3 4 5 6	funcestrcsetclem1	⊢ ( ( 𝜑 ∧ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ∈ 𝐵 ) → ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
29	22 28	syldan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
30	14	1strbas	⊢ ( 𝑏 ∈ 𝐶 → 𝑏 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → 𝑏 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
32	29 31	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) = 𝑏 )
33	32	f1oeq3d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ( ( I ↾ 𝑏 ) : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) ↔ ( I ↾ 𝑏 ) : 𝑏 –1-1-onto→ 𝑏 ) )
34	27 33	mpbiri	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ( I ↾ 𝑏 ) : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
35		resiexg	⊢ ( 𝑏 ∈ V → ( I ↾ 𝑏 ) ∈ V )
36	35	elv	⊢ ( I ↾ 𝑏 ) ∈ V
37		f1oeq1	⊢ ( 𝑖 = ( I ↾ 𝑏 ) → ( 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) ↔ ( I ↾ 𝑏 ) : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) ) )
38	36 37	spcev	⊢ ( ( I ↾ 𝑏 ) : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) → ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
39	34 38	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ } ) )
40	22 26 39	rspcedvd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → ∃ 𝑎 ∈ 𝐵 ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ 𝑎 ) )
41	40	ralrimiva	⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐶 ∃ 𝑎 ∈ 𝐵 ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ 𝑎 ) )
42	9 10 41	3jca	⊢ ( 𝜑 → ( 𝐹 ( 𝐸 Faith 𝑆 ) 𝐺 ∧ 𝐹 ( 𝐸 Full 𝑆 ) 𝐺 ∧ ∀ 𝑏 ∈ 𝐶 ∃ 𝑎 ∈ 𝐵 ∃ 𝑖 𝑖 : 𝑏 –1-1-onto→ ( 𝐹 ‘ 𝑎 ) ) )