uobeq

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

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

Proof

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

Metamath Proof Explorer

Theorem uobeq

Proof