MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  initoeu2lem1 Structured version   Visualization version   GIF version

Theorem initoeu2lem1 18068
Description: Lemma 1 for initoeu2 18070. (Contributed by AV, 9-Apr-2020.)
Hypotheses
Ref Expression
initoeu1.c (𝜑𝐶 ∈ Cat)
initoeu1.a (𝜑𝐴 ∈ (InitO‘𝐶))
initoeu2lem.x 𝑋 = (Base‘𝐶)
initoeu2lem.h 𝐻 = (Hom ‘𝐶)
initoeu2lem.i 𝐼 = (Iso‘𝐶)
initoeu2lem.o = (comp‘𝐶)
Assertion
Ref Expression
initoeu2lem1 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝐶,𝑓   𝜑,𝑓   𝐷,𝑓   𝑓,𝐹   𝑓,𝐺   𝑓,𝐼   𝑓,𝐾   𝑓,𝐻   𝑓,𝑋   ,𝑓

Proof of Theorem initoeu2lem1
StepHypRef Expression
1 eusn 4735 . . . 4 (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ↔ ∃𝑓(𝐴𝐻𝐷) = {𝑓})
2 initoeu2lem.x . . . . . . . . . . . 12 𝑋 = (Base‘𝐶)
3 eqid 2735 . . . . . . . . . . . 12 (Inv‘𝐶) = (Inv‘𝐶)
4 initoeu1.c . . . . . . . . . . . . 13 (𝜑𝐶 ∈ Cat)
54ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → 𝐶 ∈ Cat)
6 simpr2 1194 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) → 𝐵𝑋)
76adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → 𝐵𝑋)
8 simpr1 1193 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) → 𝐴𝑋)
98adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → 𝐴𝑋)
10 initoeu2lem.i . . . . . . . . . . . 12 𝐼 = (Iso‘𝐶)
112, 3, 5, 7, 9, 10invf 17816 . . . . . . . . . . 11 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → (𝐵(Inv‘𝐶)𝐴):(𝐵𝐼𝐴)⟶(𝐴𝐼𝐵))
12 simpr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → 𝐾 ∈ (𝐵𝐼𝐴))
1311, 12ffvelcdmd 7105 . . . . . . . . . 10 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵))
14 initoeu2lem.h . . . . . . . . . . . . . . . . . 18 𝐻 = (Hom ‘𝐶)
154adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) → 𝐶 ∈ Cat)
162, 14, 10, 15, 8, 6isohom 17824 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) → (𝐴𝐼𝐵) ⊆ (𝐴𝐻𝐵))
1716adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → (𝐴𝐼𝐵) ⊆ (𝐴𝐻𝐵))
1817sselda 3995 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵))
19 initoeu2lem.o . . . . . . . . . . . . . . . . . 18 = (comp‘𝐶)
2015ad4antr 732 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐶 ∈ Cat)
218ad4antr 732 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐴𝑋)
226ad4antr 732 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐵𝑋)
23 simpr3 1195 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) → 𝐷𝑋)
2423ad4antr 732 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐷𝑋)
25 simplr 769 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵))
26 simpr 484 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 ∈ (𝐵𝐻𝐷))
272, 14, 19, 20, 21, 22, 24, 25, 26catcocl 17730 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷))
2815ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → 𝐶 ∈ Cat)
298ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → 𝐴𝑋)
306ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → 𝐵𝑋)
3123ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → 𝐷𝑋)
32 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵))
33 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))
342, 14, 19, 28, 29, 30, 31, 32, 33catcocl 17730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷))
3534exp31 419 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) → (((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷))))
3635ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → (((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷))))
3736imp 406 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷)))
38 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴𝐻𝐷) = {𝑓} → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ {𝑓}))
3938adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ {𝑓}))
40 ovex 7464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ V
41 elsng 4645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ V → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ {𝑓} ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓))
4240, 41mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ {𝑓} ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓))
4339, 42bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓))
44 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴𝐻𝐷) = {𝑓} → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) ↔ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ {𝑓}))
45 ovex 7464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ V
46 elsng 4645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ V → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ {𝑓} ↔ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓))
4745, 46mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴𝐻𝐷) = {𝑓} → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ {𝑓} ↔ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓))
4844, 47bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐴𝐻𝐷) = {𝑓} → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) ↔ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓))
4948adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) ↔ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓))
50 eqeq2 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))))
5150eqcoms 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))))
5251adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 ↔ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))))
53 simp-4l 783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) ∧ (𝐺 ∈ (𝐵𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷))) → (𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)))
54 simp-4r 784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) ∧ (𝐺 ∈ (𝐵𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷))) → 𝐾 ∈ (𝐵𝐼𝐴))
55 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) ∧ (𝐺 ∈ (𝐵𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷))) → 𝐹 ∈ (𝐴𝐻𝐷))
56 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) ∧ (𝐺 ∈ (𝐵𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷))) → 𝐺 ∈ (𝐵𝐻𝐷))
57 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) ∧ (𝐺 ∈ (𝐵𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷))) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)))
58 initoeu1.a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝐴 ∈ (InitO‘𝐶))
594, 58, 2, 14, 10, 19initoeu2lem0 18067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) ∧ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))
6053, 54, 55, 56, 57, 59syl131anc 1382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾))) ∧ (𝐺 ∈ (𝐵𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))
6160exp43 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))
6261adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))
6352, 62sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))
6463ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
6564adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
6649, 65sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
6766com23 86 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) = 𝑓 → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
6843, 67sylbid 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
6968com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ (𝐴𝐻𝐷) = {𝑓}) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
7069ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))))
7170com24 95 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))))
7271adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) → (((𝐹(⟨𝐵, 𝐴 𝐷)𝐾)(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))))
7337, 72syld 47 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → (𝐺 ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))))
7473com25 99 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) → (𝐺 ∈ (𝐵𝐻𝐷) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))))
7574imp 406 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝐺(⟨𝐴, 𝐵 𝐷)((𝐵(Inv‘𝐶)𝐴)‘𝐾)) ∈ (𝐴𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
7627, 75mpd 15 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))
7776ex 412 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐻𝐵)) → (𝐺 ∈ (𝐵𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
7818, 77mpdan 687 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → (𝐺 ∈ (𝐵𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → (𝐹 ∈ (𝐴𝐻𝐷) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
7978com15 101 . . . . . . . . . . . . 13 (𝐹 ∈ (𝐴𝐻𝐷) → (𝐺 ∈ (𝐵𝐻𝐷) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))))
8079imp 406 . . . . . . . . . . . 12 ((𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝐴𝐻𝐷) = {𝑓} → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))))
8180impcom 407 . . . . . . . . . . 11 (((𝐴𝐻𝐷) = {𝑓} ∧ (𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷))) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))
8281com13 88 . . . . . . . . . 10 ((((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) ∧ ((𝐵(Inv‘𝐶)𝐴)‘𝐾) ∈ (𝐴𝐼𝐵)) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → (((𝐴𝐻𝐷) = {𝑓} ∧ (𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))
8313, 82mpdan 687 . . . . . . . . 9 (((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) ∧ 𝐾 ∈ (𝐵𝐼𝐴)) → ((𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷) → (((𝐴𝐻𝐷) = {𝑓} ∧ (𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))
8483expimpd 453 . . . . . . . 8 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋)) → ((𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷)) → (((𝐴𝐻𝐷) = {𝑓} ∧ (𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))
85843impia 1116 . . . . . . 7 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → (((𝐴𝐻𝐷) = {𝑓} ∧ (𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))
8685com12 32 . . . . . 6 (((𝐴𝐻𝐷) = {𝑓} ∧ (𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷))) → ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))
8786ex 412 . . . . 5 ((𝐴𝐻𝐷) = {𝑓} → ((𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))
8887exlimiv 1928 . . . 4 (∃𝑓(𝐴𝐻𝐷) = {𝑓} → ((𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))
891, 88sylbi 217 . . 3 (∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) → ((𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾))))
90893impib 1115 . 2 ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))
9190com12 32 1 ((𝜑 ∧ (𝐴𝑋𝐵𝑋𝐷𝑋) ∧ (𝐾 ∈ (𝐵𝐼𝐴) ∧ (𝐹(⟨𝐵, 𝐴 𝐷)𝐾) ∈ (𝐵𝐻𝐷))) → ((∃!𝑓 𝑓 ∈ (𝐴𝐻𝐷) ∧ 𝐹 ∈ (𝐴𝐻𝐷) ∧ 𝐺 ∈ (𝐵𝐻𝐷)) → 𝐺 = (𝐹(⟨𝐵, 𝐴 𝐷)𝐾)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wex 1776  wcel 2106  ∃!weu 2566  Vcvv 3478  wss 3963  {csn 4631  cop 4637  cfv 6563  (class class class)co 7431  Basecbs 17245  Hom chom 17309  compcco 17310  Catccat 17709  Invcinv 17793  Isociso 17794  InitOcinito 18035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-cat 17713  df-cid 17714  df-sect 17795  df-inv 17796  df-iso 17797
This theorem is referenced by:  initoeu2lem2  18069
  Copyright terms: Public domain W3C validator