uobffth

Description: A fully faithful functor generates equal sets of universal objects. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	uobffth.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uobffth.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	uobffth.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	uobffth.g	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
	uobffth.y	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
	uobffth.k	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
Assertion	uobffth	⊢ ( 𝜑 → 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		uobffth.k	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
7		19.42v	⊢ ( ∃ 𝑚 ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) ↔ ( 𝜑 ∧ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) )
8		fvexd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) ∈ V )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
12		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) = ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
14	9 10 11 12 13	uptrai	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) )
15		breq2	⊢ ( 𝑛 = ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) → ( 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ↔ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ( ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑚 ) ) )
16	8 14 15	spcedv	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
17	16	exlimiv	⊢ ( ∃ 𝑚 ( 𝜑 ∧ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
18	7 17	sylbir	⊢ ( ( 𝜑 ∧ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) → ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
19		19.42v	⊢ ( ∃ 𝑛 ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) ↔ ( 𝜑 ∧ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) )
20		fvexd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑛 ) ∈ V )
21	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
22	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
23	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( 𝐾 ∘_func 𝐹 ) = 𝐺 )
24	2	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝑋 ∈ 𝐵 )
25	3	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
26		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑛 ) = ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
28	21 22 23 1 24 25 26 27	uptrar	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑛 ) )
29		breq2	⊢ ( 𝑚 = ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑛 ) → ( 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ↔ 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ( ^◡ ( 𝑋 ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ‘ 𝑛 ) ) )
30	20 28 29	spcedv	⊢ ( ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
31	30	exlimiv	⊢ ( ∃ 𝑛 ( 𝜑 ∧ 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
32	19 31	sylbir	⊢ ( ( 𝜑 ∧ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) → ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
33	18 32	impbida	⊢ ( 𝜑 → ( ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ↔ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) )
34		relup	⊢ Rel ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 )
35		releldmb	⊢ ( Rel ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) → ( 𝑧 ∈ dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ↔ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 ) )
36	34 35	ax-mp	⊢ ( 𝑧 ∈ dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ↔ ∃ 𝑚 𝑧 ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑚 )
37		relup	⊢ Rel ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 )
38		releldmb	⊢ ( Rel ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) → ( 𝑧 ∈ dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ↔ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 ) )
39	37 38	ax-mp	⊢ ( 𝑧 ∈ dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ↔ ∃ 𝑛 𝑧 ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑛 )
40	33 36 39	3bitr4g	⊢ ( 𝜑 → ( 𝑧 ∈ dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) ↔ 𝑧 ∈ dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) ) )
41	40	eqrdv	⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )

Metamath Proof Explorer

Theorem uobffth

Proof