Metamath Proof Explorer

Theorem uptrlem1

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

Ref Expression
Hypotheses uptrlem1.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
uptrlem1.i ⊢ 𝐼 = ( Hom ‘ 𝐷 )
uptrlem1.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
uptrlem1.d ⊢ ∙ = ( comp ‘ 𝐷 )
uptrlem1.e ⊢ ⚬ = ( comp ‘ 𝐸 )
uptrlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
uptrlem1.y ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) = 𝑌 )
uptrlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
uptrlem1.w ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐶 ) )
uptrlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑍 ) ) )
uptrlem1.b ⊢ ( 𝜑 → ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝐴 ) = 𝐵 )
uptrlem1.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
uptrlem1.m ⊢ ( 𝜑 → 𝑀 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑁 )
uptrlem1.k ⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
Assertion uptrlem1 ( 𝜑 → ( ∀ ℎ ∈ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ℎ = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ↔ ∀ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 uptrlem1.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
2 uptrlem1.i ⊢ 𝐼 = ( Hom ‘ 𝐷 )
3 uptrlem1.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
4 uptrlem1.d ⊢ ∙ = ( comp ‘ 𝐷 )
5 uptrlem1.e ⊢ ⚬ = ( comp ‘ 𝐸 )
6 uptrlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
7 uptrlem1.y ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) = 𝑌 )
8 uptrlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
9 uptrlem1.w ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐶 ) )
10 uptrlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑍 ) ) )
11 uptrlem1.b ⊢ ( 𝜑 → ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝐴 ) = 𝐵 )
12 uptrlem1.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
13 uptrlem1.m ⊢ ( 𝜑 → 𝑀 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑁 )
14 uptrlem1.k ⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
15 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
17 16 15 12 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
18 17 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑊 ) ∈ ( Base ‘ 𝐷 ) )
19 15 2 3 13 6 18 ffthf1o ⊢ ( 𝜑 → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ( 𝑀 ‘ 𝑋 ) 𝐽 ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) ) )
20 inss1 ⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Full 𝐸 )
21 fullfunc ⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
22 20 21 sstri ⊢ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ⊆ ( 𝐷 Func 𝐸 )
23 22 ssbri ⊢ ( 𝑀 ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) 𝑁 → 𝑀 ( 𝐷 Func 𝐸 ) 𝑁 )
24 13 23 syl ⊢ ( 𝜑 → 𝑀 ( 𝐷 Func 𝐸 ) 𝑁 )
25 16 12 24 14 9 cofu1a ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) = ( 𝐾 ‘ 𝑊 ) )
26 7 25 oveq12d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) 𝐽 ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) ) = ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
27 26 f1oeq3d ⊢ ( 𝜑 → ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ( 𝑀 ‘ 𝑋 ) 𝐽 ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) ) ↔ ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) ) )
28 19 27 mpbid ⊢ ( 𝜑 → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
29 f1of ⊢ ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ⟶ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
30 28 29 syl ⊢ ( 𝜑 → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ⟶ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
31 30 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) → ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) ∈ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
32 f1ofo ⊢ ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
33 28 32 syl ⊢ ( 𝜑 → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
34 foelrn ⊢ ( ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) ∧ ℎ ∈ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) ) → ∃ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) )
35 33 34 sylan ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) ) → ∃ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) )
36 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∧ ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) )
37 36 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∧ ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ℎ = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ↔ ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ) )
38 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑀 ( 𝐷 Func 𝐸 ) 𝑁 )
39 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑋 ∈ ( Base ‘ 𝐷 ) )
40 17 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) )
41 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( 𝐹 ‘ 𝑍 ) ∈ ( Base ‘ 𝐷 ) )
42 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( 𝐹 ‘ 𝑊 ) ∈ ( Base ‘ 𝐷 ) )
43 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝐴 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑍 ) ) )
44 16 1 2 12 8 9 funcf2 ⊢ ( 𝜑 → ( 𝑍 𝐺 𝑊 ) : ( 𝑍 𝐻 𝑊 ) ⟶ ( ( 𝐹 ‘ 𝑍 ) 𝐼 ( 𝐹 ‘ 𝑊 ) ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) → ( 𝑍 𝐺 𝑊 ) : ( 𝑍 𝐻 𝑊 ) ⟶ ( ( 𝐹 ‘ 𝑍 ) 𝐼 ( 𝐹 ‘ 𝑊 ) ) )
46 45 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ∈ ( ( 𝐹 ‘ 𝑍 ) 𝐼 ( 𝐹 ‘ 𝑊 ) ) )
47 15 2 4 5 38 39 41 42 43 46 funcco ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) = ( ( ( ( 𝐹 ‘ 𝑍 ) 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ) ( ⟨ ( 𝑀 ‘ 𝑋 ) , ( 𝑀 ‘ ( 𝐹 ‘ 𝑍 ) ) ⟩ ⚬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) ) ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝐴 ) ) )
48 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( 𝑀 ‘ 𝑋 ) = 𝑌 )
49 16 12 24 14 8 cofu1a ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑍 ) ) = ( 𝐾 ‘ 𝑍 ) )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑍 ) ) = ( 𝐾 ‘ 𝑍 ) )
51 48 50 opeq12d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ⟨ ( 𝑀 ‘ 𝑋 ) , ( 𝑀 ‘ ( 𝐹 ‘ 𝑍 ) ) ⟩ = ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ )
52 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) = ( 𝐾 ‘ 𝑊 ) )
53 51 52 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ⟨ ( 𝑀 ‘ 𝑋 ) , ( 𝑀 ‘ ( 𝐹 ‘ 𝑍 ) ) ⟩ ⚬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) ) = ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) )
54 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
55 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ⟨ 𝑀 , 𝑁 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩ )
56 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
57 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐶 ) )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) )
59 16 54 38 55 56 57 1 58 cofu2a ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( ( 𝐹 ‘ 𝑍 ) 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ) = ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) )
60 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝐴 ) = 𝐵 )
61 53 59 60 oveq123d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( ( ( 𝐹 ‘ 𝑍 ) 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ) ( ⟨ ( 𝑀 ‘ 𝑋 ) , ( 𝑀 ‘ ( 𝐹 ‘ 𝑍 ) ) ⟩ ⚬ ( 𝑀 ‘ ( 𝐹 ‘ 𝑊 ) ) ) ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑍 ) ) ‘ 𝐴 ) ) = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) )
62 47 61 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) )
63 62 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) ↔ ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ) )
64 f1of1 ⊢ ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
65 28 64 syl ⊢ ( 𝜑 → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) )
67 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) )
68 38 funcrcl2 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝐷 ∈ Cat )
69 15 2 4 68 39 41 42 43 46 catcocl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) )
70 f1fveq ⊢ ( ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) : ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) –1-1→ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) ∧ ( 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∧ ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ) → ( ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) ↔ 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )
71 66 67 69 70 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) ↔ 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )
72 63 71 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ↔ 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )
73 72 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∧ ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ↔ 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )
74 37 73 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∧ ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) ) ∧ 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ℎ = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ↔ 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )
75 74 reubidva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∧ ℎ = ( ( 𝑋 𝑁 ( 𝐹 ‘ 𝑊 ) ) ‘ 𝑔 ) ) → ( ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ℎ = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ↔ ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )
76 31 35 75 ralxfrd2 ⊢ ( 𝜑 → ( ∀ ℎ ∈ ( 𝑌 𝐽 ( 𝐾 ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) ℎ = ( ( ( 𝑍 𝐿 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑌 , ( 𝐾 ‘ 𝑍 ) ⟩ ⚬ ( 𝐾 ‘ 𝑊 ) ) 𝐵 ) ↔ ∀ 𝑔 ∈ ( 𝑋 𝐼 ( 𝐹 ‘ 𝑊 ) ) ∃! 𝑘 ∈ ( 𝑍 𝐻 𝑊 ) 𝑔 = ( ( ( 𝑍 𝐺 𝑊 ) ‘ 𝑘 ) ( ⟨ 𝑋 , ( 𝐹 ‘ 𝑍 ) ⟩ ∙ ( 𝐹 ‘ 𝑊 ) ) 𝐴 ) ) )