uobeqw

Description: If a full functor (in fact, a full embedding) is a section of a fully faithful functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uobffth.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uobffth.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	uobffth.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	uobffth.g	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
	uobffth.y	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
	uobeq.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
	uobeq.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
	uobeq.n	⊢ ( 𝜑 → ( 𝐿 ∘_func 𝐾 ) = 𝐼 )
	uobeqw.l	⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐸 Full 𝐷 ) ∩ ( 𝐸 Faith 𝐷 ) ) )
Assertion	uobeqw	⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		uobffth.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		uobffth.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3		uobffth.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4		uobffth.g	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
5		uobffth.y	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
6		uobeq.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
7		uobeq.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
8		uobeq.n	⊢ ( 𝜑 → ( 𝐿 ∘_func 𝐾 ) = 𝐼 )
9		uobeqw.l	⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐸 Full 𝐷 ) ∩ ( 𝐸 Faith 𝐷 ) ) )
10		19.42v	⊢ ( ∃ 𝑚 ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) ↔ ( 𝜑 ∧ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) )
11		fvexd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) ∈ V )
12	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
13		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
14		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
15	14 7	sselid	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
16		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
17	13 15 16	sylancr	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
18	15	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
19		inss1	⊢ ( ( 𝐸 Full 𝐷 ) ∩ ( 𝐸 Faith 𝐷 ) ) ⊆ ( 𝐸 Full 𝐷 )
20		fullfunc	⊢ ( 𝐸 Full 𝐷 ) ⊆ ( 𝐸 Func 𝐷 )
21	19 20	sstri	⊢ ( ( 𝐸 Full 𝐷 ) ∩ ( 𝐸 Faith 𝐷 ) ) ⊆ ( 𝐸 Func 𝐷 )
22	21 9	sselid	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐸 Func 𝐷 ) )
23	22	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐸 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
24	15 22	cofu1st2nd	⊢ ( 𝜑 → ( 𝐿 ∘_func 𝐾 ) = ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
25	24 8	eqtr3d	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) = 𝐼 )
26	6 18 23 25	cofidfth	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Faith 𝐸 ) ( 2^nd ‘ 𝐾 ) )
27		df-br	⊢ ( ( 1^st ‘ 𝐾 ) ( 𝐷 Faith 𝐸 ) ( 2^nd ‘ 𝐾 ) ↔ ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∈ ( 𝐷 Faith 𝐸 ) )
28	26 27	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ∈ ( 𝐷 Faith 𝐸 ) )
29	17 28	eqeltrd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Faith 𝐸 ) )
30	7 29	elind	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
32	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
33		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) = ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) )
34		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
35	12 31 32 33 34	uptrai	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) )
36		breq2	⊢ ( 𝑛 = ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) → ( 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ↔ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) ) )
37	11 35 36	spcedv	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
38	37	exlimiv	⊢ ( ∃ 𝑚 ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
39	10 38	sylbir	⊢ ( ( 𝜑 ∧ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
40		19.42v	⊢ ( ∃ 𝑛 ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) ↔ ( 𝜑 ∧ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) )
41		fvexd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( ( 𝑌 ( 2^nd ‘ 𝐿 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ V )
42	5	fveq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) )
43	6 1 2 15 22 8	cofid1a	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
44	42 43	eqtr3d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) = 𝑋 )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑌 ) = 𝑋 )
46	9	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝐿 ∈ ( ( 𝐸 Full 𝐷 ) ∩ ( 𝐸 Faith 𝐷 ) ) )
47	3 15 22	cofuass	⊢ ( 𝜑 → ( ( 𝐿 ∘_func 𝐾 ) ∘_func 𝐹 ) = ( 𝐿 ∘_func ( 𝐾 ∘_func 𝐹 ) ) )
48	8	oveq1d	⊢ ( 𝜑 → ( ( 𝐿 ∘_func 𝐾 ) ∘_func 𝐹 ) = ( 𝐼 ∘_func 𝐹 ) )
49	3 6	cofulid	⊢ ( 𝜑 → ( 𝐼 ∘_func 𝐹 ) = 𝐹 )
50	48 49	eqtrd	⊢ ( 𝜑 → ( ( 𝐿 ∘_func 𝐾 ) ∘_func 𝐹 ) = 𝐹 )
51	4	oveq2d	⊢ ( 𝜑 → ( 𝐿 ∘_func ( 𝐾 ∘_func 𝐹 ) ) = ( 𝐿 ∘_func 𝐺 ) )
52	47 50 51	3eqtr3rd	⊢ ( 𝜑 → ( 𝐿 ∘_func 𝐺 ) = 𝐹 )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( 𝐿 ∘_func 𝐺 ) = 𝐹 )
54		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( ( 𝑌 ( 2^nd ‘ 𝐿 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ( 𝑌 ( 2^nd ‘ 𝐿 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
55		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
56	45 46 53 54 55	uptrai	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ( ( 𝑌 ( 2^nd ‘ 𝐿 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
57		breq2	⊢ ( 𝑚 = ( ( 𝑌 ( 2^nd ‘ 𝐿 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑛 ) → ( 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ↔ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ( ( 𝑌 ( 2^nd ‘ 𝐿 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑛 ) ) )
58	41 56 57	spcedv	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
59	58	exlimiv	⊢ ( ∃ 𝑛 ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
60	40 59	sylbir	⊢ ( ( 𝜑 ∧ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
61	39 60	impbida	⊢ ( 𝜑 → ( ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ↔ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) )
62		relup	⊢ Rel ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 )
63		releldmb	⊢ ( Rel ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) → ( 𝑧 ∈ dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ↔ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) )
64	62 63	ax-mp	⊢ ( 𝑧 ∈ dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ↔ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
65		relup	⊢ Rel ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 )
66		releldmb	⊢ ( Rel ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) → ( 𝑧 ∈ dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ↔ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) )
67	65 66	ax-mp	⊢ ( 𝑧 ∈ dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ↔ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
68	61 64 67	3bitr4g	⊢ ( 𝜑 → ( 𝑧 ∈ dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ↔ 𝑧 ∈ dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ) )
69	68	eqrdv	⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )

Metamath Proof Explorer

Theorem uobeqw

Proof