Metamath Proof Explorer

Theorem upciclem4

Description: Lemma for upcic and upeu . (Contributed by Zhi Wang, 19-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 ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
upcic.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
upcic.2 ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
Assertion upciclem4 ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 ∧ ∃ 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )

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 upcic.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
13 upcic.2 ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
14 11 8 12 upciclem1 ⊢ ( 𝜑 → ∃! 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
15 reurex ⊢ ( ∃! 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) → ∃ 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
16 14 15 syl ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
17 simpl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) → 𝜑 )
18 13 7 10 upciclem1 ⊢ ( 𝜑 → ∃! 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) )
19 reurex ⊢ ( ∃! 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) → ∃ 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) )
20 17 18 19 3syl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) → ∃ 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) )
21 eqid ⊢ ( Iso ‘ 𝐷 ) = ( Iso ‘ 𝐷 )
22 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
23 22 funcrcl2 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝐷 ∈ Cat )
24 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑋 ∈ 𝐵 )
25 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑌 ∈ 𝐵 )
26 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
27 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
28 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) )
29 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) )
30 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑍 ∈ 𝐶 )
31 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
32 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
33 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) )
34 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
35 1 2 3 4 5 22 24 25 30 31 32 26 28 29 33 34 upciclem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → ( 𝑞 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑋 ) 𝑝 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) )
36 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
37 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
38 1 2 3 4 5 22 25 24 30 36 37 26 29 28 34 33 upciclem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → ( 𝑝 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐷 ) 𝑌 ) 𝑞 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) )
39 1 3 26 21 27 23 24 25 28 29 35 38 isisod ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑝 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) )
40 21 1 23 24 25 39 brcici ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) ∧ ( 𝑞 ∈ ( 𝑌 𝐻 𝑋 ) ∧ 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑞 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) ) ) → 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 )
41 20 40 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) → 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 )
42 16 41 rexlimddv ⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 )
43 20 39 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) → 𝑝 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) )
44 simprr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( 𝑋 𝐻 𝑌 ) ∧ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) ) → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
45 16 43 44 reximssdv ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
46 fveq2 ⊢ ( 𝑝 = 𝑟 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) )
47 46 oveq1d ⊢ ( 𝑝 = 𝑟 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
48 47 eqeq2d ⊢ ( 𝑝 = 𝑟 → ( 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
49 48 cbvrexvw ⊢ ( ∃ 𝑝 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ∃ 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
50 45 49 sylib ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
51 42 50 jca ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 ∧ ∃ 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )