Metamath Proof Explorer

Theorem initoeu2lem0

Description: Lemma 0 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 initoeu2lem0 ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )

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 3simpa ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) )
8 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) → ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) )
9 8 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) )
10 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
11 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐶 ∈ Cat )
12 11 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐶 ∈ Cat )
13 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
14 13 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐴 ∈ 𝑋 )
15 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐵 ∈ 𝑋 )
17 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐷 ∈ 𝑋 )
18 5 oveqi ⊢ ( 𝐵 𝐼 𝐴 ) = ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 )
19 18 eleq2i ⊢ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ↔ 𝐾 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) )
20 19 biimpi ⊢ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) → 𝐾 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) )
21 20 3ad2ant1 ⊢ ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐾 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) )
22 21 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐾 ∈ ( 𝐵 ( Iso ‘ 𝐶 ) 𝐴 ) )
23 4 oveqi ⊢ ( 𝐵 𝐻 𝐷 ) = ( 𝐵 ( Hom ‘ 𝐶 ) 𝐷 )
24 23 eleq2i ⊢ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ↔ 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐷 ) )
25 24 biimpi ⊢ ( 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) → 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐷 ) )
26 25 3ad2ant3 ⊢ ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐷 ) )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐺 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐷 ) )
28 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
29 3 28 5 11 15 13 isohom ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( 𝐵 𝐼 𝐴 ) ⊆ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
30 29 sseld ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) → 𝐾 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
31 30 com12 ⊢ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐾 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
32 31 3ad2ant1 ⊢ ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → 𝐾 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) ) )
33 32 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐾 ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐴 ) )
34 4 oveqi ⊢ ( 𝐴 𝐻 𝐷 ) = ( 𝐴 ( Hom ‘ 𝐶 ) 𝐷 )
35 34 eleq2i ⊢ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ↔ 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐷 ) )
36 35 biimpi ⊢ ( 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) → 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐷 ) )
37 36 3ad2ant2 ⊢ ( ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) → 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐷 ) )
38 37 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → 𝐹 ∈ ( 𝐴 ( Hom ‘ 𝐶 ) 𝐷 ) )
39 3 28 6 12 16 14 17 33 38 catcocl ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ∈ ( 𝐵 ( Hom ‘ 𝐶 ) 𝐷 ) )
40 eqid ⊢ ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) = ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 )
41 6 oveqi ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) = ( ⟨ 𝐴 , 𝐵 ⟩ ( comp ‘ 𝐶 ) 𝐷 )
42 3 10 12 14 16 17 22 27 39 40 41 rcaninv ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ) → ( ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ) )
43 7 9 42 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ∧ ( 𝐾 ∈ ( 𝐵 𝐼 𝐴 ) ∧ 𝐹 ∈ ( 𝐴 𝐻 𝐷 ) ∧ 𝐺 ∈ ( 𝐵 𝐻 𝐷 ) ) ∧ ( ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) = ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ ⚬ 𝐷 ) ( ( 𝐵 ( Inv ‘ 𝐶 ) 𝐴 ) ‘ 𝐾 ) ) ) → 𝐺 = ( 𝐹 ( ⟨ 𝐵 , 𝐴 ⟩ ⚬ 𝐷 ) 𝐾 ) )