Metamath Proof Explorer

Theorem upeu2

Description: Generate new universal morphism through isomorphism from existing universal object. (Contributed by Zhi Wang, 20-Sep-2025)

Ref Expression
Hypotheses upcic.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
upcic.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
upcic.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
upcic.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
upcic.o ⊢ 𝑂 = ( comp ‘ 𝐸 )
upcic.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
upcic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
upcic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
upcic.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐶 )
upcic.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
upcic.1 ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
upeu2.i ⊢ 𝐼 = ( Iso ‘ 𝐷 )
upeu2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐼 𝑌 ) )
upeu2.n ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
Assertion upeu2 ( 𝜑 → ( 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∧ ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 upcic.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 upcic.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
3 upcic.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
4 upcic.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
5 upcic.o ⊢ 𝑂 = ( comp ‘ 𝐸 )
6 upcic.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
7 upcic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 upcic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 upcic.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐶 )
10 upcic.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
11 upcic.1 ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
12 upeu2.i ⊢ 𝐼 = ( Iso ‘ 𝐷 )
13 upeu2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐼 𝑌 ) )
14 upeu2.n ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
15 6 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
16 1 2 6 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
17 16 7 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐶 )
18 16 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ 𝐶 )
19 1 3 4 6 7 8 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
20 6 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
21 1 3 12 20 7 8 isohom ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )
22 21 13 sseldd ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
23 19 22 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
24 2 4 5 15 9 17 18 10 23 catcocl ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
25 14 24 eqeltrd ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
26 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
27 simprl ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) → 𝑣 ∈ 𝐵 )
28 simprr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) → 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) )
29 26 27 28 upciclem1 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) → ∃! 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑋 𝐺 𝑣 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑀 ) )
30 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
31 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ) → 𝐷 ∈ Cat )
32 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ) → 𝑋 ∈ 𝐵 )
33 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ) → 𝑌 ∈ 𝐵 )
34 27 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ) → 𝑣 ∈ 𝐵 )
35 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ) → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
36 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ) → 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) )
37 1 3 30 31 32 33 34 35 36 catcocl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ) → ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ∈ ( 𝑋 𝐻 𝑣 ) )
38 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) ) → 𝐷 ∈ Cat )
39 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) ) → 𝑋 ∈ 𝐵 )
40 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) ) → 𝑌 ∈ 𝐵 )
41 27 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) ) → 𝑣 ∈ 𝐵 )
42 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) ) → 𝐾 ∈ ( 𝑋 𝐼 𝑌 ) )
43 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) ) → 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) )
44 1 3 30 12 38 39 40 41 42 43 upeu2lem ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) ) → ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) )
45 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → ( ( 𝑋 𝐺 𝑣 ) ‘ 𝑝 ) = ( ( 𝑋 𝐺 𝑣 ) ‘ ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) )
47 46 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → ( ( ( 𝑋 𝐺 𝑣 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑣 ) ‘ ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑀 ) )
48 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
49 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑋 ∈ 𝐵 )
50 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑌 ∈ 𝐵 )
51 27 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑣 ∈ 𝐵 )
52 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑍 ∈ 𝐶 )
53 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
54 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
55 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) )
56 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
57 1 2 3 4 5 48 49 50 51 52 53 30 54 55 56 upciclem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → ( ( ( 𝑋 𝐺 𝑣 ) ‘ ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑀 ) = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
58 47 57 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → ( ( ( 𝑋 𝐺 𝑣 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑀 ) = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
59 58 eqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) ∧ ( 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) ∧ 𝑝 = ( 𝑙 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑣 ) 𝐾 ) ) ) → ( 𝑔 = ( ( ( 𝑋 𝐺 𝑣 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑀 ) ↔ 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) ) )
60 37 44 59 reuxfr1dd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) → ( ∃! 𝑝 ∈ ( 𝑋 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑋 𝐺 𝑣 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑀 ) ↔ ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) ) )
61 29 60 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ) ) → ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
62 61 ralrimivva ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
63 25 62 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∧ ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) ) )