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

Metamath Proof Explorer

Theorem initoeu2lem1

Description: Lemma 1 for initoeu2 . (Contributed by AV, 9-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
initoeu2lem.x ⊢ 𝑋 = ( Base ‘ 𝐶 )
initoeu2lem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
initoeu2lem.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
initoeu2lem.o ⊢ ⚬ = ( comp ‘ 𝐶 )
Assertion initoeu2lem1 ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
3 initoeu2lem.x ⊢ 𝑋 = ( Base ‘ 𝐶 )
4 initoeu2lem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 initoeu2lem.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
6 initoeu2lem.o ⊢ ⚬ = ( comp ‘ 𝐶 )
7 eusn ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ↔ ∃ 𝑓 ( 𝐴 𝐻 𝐷 ) = { 𝑓 } )
8 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
9 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐶 ∈ Cat )
10 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
11 10 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐵 ∈ 𝑋 )
12 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
13 12 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑋 )
14 3 8 9 11 13 5 invf ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) : ( 𝐵 𝐼 𝐴 ) ⟶ ( 𝐴 𝐼 𝐵 ) )
15 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) )
16 14 15 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) )
17 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐶 ∈ Cat )
18 3 4 5 17 12 10 isohom ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( 𝐴 𝐼 𝐵 ) ⊆ ( 𝐴 𝐻 𝐵 ) )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → ( 𝐴 𝐼 𝐵 ) ⊆ ( 𝐴 𝐻 𝐵 ) )
20 19 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) )
21 17 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐶 ∈ Cat )
22 12 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐴 ∈ 𝑋 )
23 10 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐵 ∈ 𝑋 )
24 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐷 ∈ 𝑋 )
25 24 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐷 ∈ 𝑋 )
26 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) )
27 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) )
28 3 4 6 21 22 23 25 26 27 catcocl ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) )
29 17 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐶 ∈ Cat )
30 12 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐴 ∈ 𝑋 )
31 10 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐵 ∈ 𝑋 )
32 24 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐷 ∈ 𝑋 )
33 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) )
34 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) )
35 3 4 6 29 30 31 32 33 34 catcocl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) )
36 35 exp31 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ) ) )
37 36 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ) ) )
38 37 imp ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ) )
39 eleq2 ⊢ ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ { 𝑓 } ) )
40 39 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ { 𝑓 } ) )
41 ovex ⊢ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ V
42 elsng ⊢ ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ V → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ { 𝑓 } ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) )
43 41 42 mp1i ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ { 𝑓 } ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) )
44 40 43 bitrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) )
45 eleq2 ⊢ ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ↔ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ { 𝑓 } ) )
46 ovex ⊢ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ V
47 elsng ⊢ ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ V → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ { 𝑓 } ↔ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) )
48 46 47 mp1i ⊢ ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ { 𝑓 } ↔ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) )
49 45 48 bitrd ⊢ ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ↔ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) )
50 49 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) ↔ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) )
51 eqeq2 ⊢ ( 𝑓 = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) )
52 51 eqcoms ⊢ ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) )
53 52 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ↔ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) )
54 simp-4l ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) ∧ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ) ) → ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) )
55 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) ∧ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ) ) → 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) )
56 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) ∧ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ) ) → 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) )
57 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) ∧ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ) ) → 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) )
58 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) ∧ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) )
59 1 2 3 4 5 6 initoeu2lem0 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
60 54 55 56 57 58 59 syl131anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) ∧ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )
61 60 exp43 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) )
62 61 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) )
63 53 62 sylbid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) )
64 63 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
65 64 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
66 50 65 sylbid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
67 66 com23 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = 𝑓 → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
68 44 67 sylbid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
69 68 com23 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
70 69 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) ) )
71 70 com24 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) ) )
72 71 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) → ( ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) ) )
73 38 72 syld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) ) )
74 73 com25 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) ) )
75 74 imp ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
76 28 75 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) )
77 76 ex ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐻 𝐵 ) ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
78 20 77 mpdan ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
79 78 com15 ⊢ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) ) )
80 79 imp ⊢ ( ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) ) )
81 80 impcom ⊢ ( ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ∧ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) )
82 81 com13 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) ∧ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ∈ ( 𝐴 𝐼 𝐵 ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ∧ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) )
83 16 82 mpdan ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) → ( ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ∧ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) )
84 83 expimpd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ∧ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) )
85 84 3impia ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ∧ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )
86 85 com12 ⊢ ( ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } ∧ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )
87 86 ex ⊢ ( ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) )
88 87 exlimiv ⊢ ( ∃ 𝑓 ( 𝐴 𝐻 𝐷 ) = { 𝑓 } → ( ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) )
89 7 88 sylbi ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) → ( ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) ) )
90 89 3impib ⊢ ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )
91 90 com12 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( ∃! 𝑓 𝑓 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )