This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐸 ) 𝑌 ) 𝑁 ) )