Theorem uptrlem3

Description: Lemma for uptr . (Contributed by Zhi Wang, 16-Nov-2025)

	Ref	Expression
Hypotheses	uptr.y	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
	uptr.r	⊢ ( 𝜑 → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
	uptr.k	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
	uptr.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uptr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	uptr.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	uptr.n	⊢ ( 𝜑 → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
	uptr.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	uptr.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
	uptrlem3.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	uptrlem3.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
Assertion	uptrlem3	⊢ ( 𝜑 → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		uptr.y	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
2		uptr.r	⊢ ( 𝜑 → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
3		uptr.k	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
4		uptr.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		uptr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		uptr.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7		uptr.n	⊢ ( 𝜑 → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
8		uptr.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
9		uptr.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
10		uptrlem3.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
11		uptrlem3.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
12		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
14		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
15		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
16	5 4	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑋 ∈ ( Base ‘ 𝐷 ) )
18	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑅 ‘ 𝑋 ) = 𝑌 )
19	11 10	eleqtrdi	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
22	21 10	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
23	9	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑀 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
24	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) = 𝑁 )
25	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
26	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 )
27	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
28	12 8 13 14 15 17 18 20 22 23 24 25 26 27	uptrlem1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑦 ) ℎ = ( ( ( 𝑍 𝐿 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑁 ) ↔ ∀ 𝑔 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑦 ) 𝑔 = ( ( ( 𝑍 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ) )
29	28	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑦 ) ℎ = ( ( ( 𝑍 𝐿 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑁 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑔 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑦 ) 𝑔 = ( ( ( 𝑍 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ) )
30		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
31		inss1	⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Full 𝐸 )
32		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
33	31 32	sstri	⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Func 𝐸 )
34	33	ssbri	⊢ ( 𝑅 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑆 → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
35	2 34	syl	⊢ ( 𝜑 → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
36	4 30 35	funcf1	⊢ ( 𝜑 → 𝑅 : 𝐵 ⟶ ( Base ‘ 𝐸 ) )
37	36 5	ffvelcdmd	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑋 ) ∈ ( Base ‘ 𝐸 ) )
38	1 37	eqeltrrd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐸 ) )
39	6 35	cofucla	⊢ ( 𝜑 → ( ⟨ 𝑅 , 𝑆 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( 𝐶 Func 𝐸 ) )
40	3 39	eqeltrrd	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
41		df-br	⊢ ( 𝐾 ( 𝐶 Func 𝐸 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
42	40 41	sylibr	⊢ ( 𝜑 → 𝐾 ( 𝐶 Func 𝐸 ) 𝐿 )
43	10 4 6	funcf1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
44	43 11	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑍 ) ∈ 𝐵 )
45	4 8 13 35 5 44	funcf2	⊢ ( 𝜑 → ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) : ( 𝑋 𝐽 ( 𝐹 ‘ 𝑍 ) ) ⟶ ( ( 𝑅 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝐹 ‘ 𝑍 ) ) ) )
46	45 9	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑋 𝑆 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝑀 ) ∈ ( ( 𝑅 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝐹 ‘ 𝑍 ) ) ) )
47	10 6 35 3 11	cofu1a	⊢ ( 𝜑 → ( 𝑅 ‘ ( 𝐹 ‘ 𝑍 ) ) = ( 𝐾 ‘ 𝑍 ) )
48	1 47	oveq12d	⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝐹 ‘ 𝑍 ) ) ) = ( 𝑌 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑍 ) ) )
49	46 7 48	3eltr3d	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑍 ) ) )
50	10 30 12 13 15 38 42 11 49	isup	⊢ ( 𝜑 → ( 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ↔ ∀ 𝑦 ∈ 𝐴 ∀ ℎ ∈ ( 𝑌 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑦 ) ℎ = ( ( ( 𝑍 𝐿 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑁 ) ) )
51	10 4 12 8 14 5 6 11 9	isup	⊢ ( 𝜑 → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑔 ∈ ( 𝑋 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑦 ) 𝑔 = ( ( ( 𝑍 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ) )
52	29 50 51	3bitr4rd	⊢ ( 𝜑 → ( 𝑍 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐷 ) 𝑋 ) 𝑀 ↔ 𝑍 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐶 UP 𝐸 ) 𝑌 ) 𝑁 ) )