Theorem upeu2lem 48877

Description: Lemma for upeu2 48928. There exists a unique morphism from 𝑌 to 𝑍 that commutes if 𝐹:𝑋⟶𝑌 is an isomorphism. (Contributed by Zhi Wang, 20-Sep-2025.)

Hypotheses

Ref	Expression
upeu2lem.b	⊢ 𝐵 = (Base‘𝐶)
upeu2lem.h	⊢ 𝐻 = (Hom ‘𝐶)
upeu2lem.o	⊢ · = (comp‘𝐶)
upeu2lem.i	⊢ 𝐼 = (Iso‘𝐶)
upeu2lem.c	⊢ (𝜑 → 𝐶 ∈ Cat)
upeu2lem.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
upeu2lem.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
upeu2lem.z	⊢ (𝜑 → 𝑍 ∈ 𝐵)
upeu2lem.f	⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))
upeu2lem.g	⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑍))

Assertion

Ref	Expression
upeu2lem	⊢ (𝜑 → ∃!𝑘 ∈ (𝑌𝐻𝑍)𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))

Distinct variable groups:   · ,𝑘   𝐶,𝑘   𝑘,𝐹   𝑘,𝐺   𝑘,𝐻   𝑘,𝑋   𝑘,𝑌   𝑘,𝑍   𝜑,𝑘

Allowed substitution hints:   𝐵(𝑘)   𝐼(𝑘)

Proof of Theorem upeu2lem

Step	Hyp	Ref	Expression
1		upeu2lem.b	. . 3 ⊢ 𝐵 = (Base‘𝐶)
2		upeu2lem.h	. . 3 ⊢ 𝐻 = (Hom ‘𝐶)
3		upeu2lem.o	. . 3 ⊢ · = (comp‘𝐶)
4		upeu2lem.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
5		upeu2lem.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
6		upeu2lem.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
7		upeu2lem.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝐵)
8		upeu2lem.i	. . . . 5 ⊢ 𝐼 = (Iso‘𝐶)
9	1, 2, 8, 4, 5, 6	isohom 17774	. . . 4 ⊢ (𝜑 → (𝑌𝐼𝑋) ⊆ (𝑌𝐻𝑋))
10		eqid 2734	. . . . . 6 ⊢ (Inv‘𝐶) = (Inv‘𝐶)
11	1, 10, 4, 6, 5, 8	invf 17766	. . . . 5 ⊢ (𝜑 → (𝑋(Inv‘𝐶)𝑌):(𝑋𝐼𝑌)⟶(𝑌𝐼𝑋))
12		upeu2lem.f	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐼𝑌))
13	11, 12	ffvelcdmd 7071	. . . 4 ⊢ (𝜑 → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌𝐼𝑋))
14	9, 13	sseldd 3957	. . 3 ⊢ (𝜑 → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌𝐻𝑋))
15		upeu2lem.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ (𝑋𝐻𝑍))
16	1, 2, 3, 4, 5, 6, 7, 14, 15	catcocl 17682	. 2 ⊢ (𝜑 → (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) ∈ (𝑌𝐻𝑍))
17		oveq1 7406	. . . . . 6 ⊢ (𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) → (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
18	17	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) ∧ 𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)) → (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
19	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝐶 ∈ Cat)
20	5	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝑌 ∈ 𝐵)
21	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝑋 ∈ 𝐵)
22	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌𝐻𝑋))
23	1, 2, 8, 4, 6, 5	isohom 17774	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌))
24	23, 12	sseldd 3957	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌))
25	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝐹 ∈ (𝑋𝐻𝑌))
26	7	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝑍 ∈ 𝐵)
27		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝑘 ∈ (𝑌𝐻𝑍))
28	1, 2, 3, 19, 20, 21, 20, 22, 25, 26, 27	catass 17683	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → ((𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = (𝑘(⟨𝑌, 𝑌⟩ · 𝑍)(𝐹(⟨𝑌, 𝑋⟩ · 𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹))))
29	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝐹 ∈ (𝑋𝐼𝑌))
30		eqid 2734	. . . . . . . . 9 ⊢ (Id‘𝐶) = (Id‘𝐶)
31	3	oveqi 7412	. . . . . . . . 9 ⊢ (⟨𝑌, 𝑋⟩ · 𝑌) = (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)
32	1, 8, 10, 19, 21, 20, 29, 30, 31	isocoinvid 17791	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → (𝐹(⟨𝑌, 𝑋⟩ · 𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((Id‘𝐶)‘𝑌))
33	32	oveq2d 7415	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → (𝑘(⟨𝑌, 𝑌⟩ · 𝑍)(𝐹(⟨𝑌, 𝑋⟩ · 𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = (𝑘(⟨𝑌, 𝑌⟩ · 𝑍)((Id‘𝐶)‘𝑌)))
34	1, 2, 30, 19, 20, 3, 26, 27	catrid 17681	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → (𝑘(⟨𝑌, 𝑌⟩ · 𝑍)((Id‘𝐶)‘𝑌)) = 𝑘)
35	28, 33, 34	3eqtrd 2773	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → ((𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = 𝑘)
36	35	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) ∧ 𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)) → ((𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = 𝑘)
37	18, 36	eqtr2d 2770	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) ∧ 𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹)) → 𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
38		oveq1 7406	. . . . . 6 ⊢ (𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) → (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = ((𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
39	38	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) ∧ 𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))) → (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = ((𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
40	15	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → 𝐺 ∈ (𝑋𝐻𝑍))
41	1, 2, 3, 19, 21, 20, 21, 25, 22, 26, 40	catass 17683	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → ((𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = (𝐺(⟨𝑋, 𝑋⟩ · 𝑍)(((𝑋(Inv‘𝐶)𝑌)‘𝐹)(⟨𝑋, 𝑌⟩ · 𝑋)𝐹)))
42	3	oveqi 7412	. . . . . . . . 9 ⊢ (⟨𝑋, 𝑌⟩ · 𝑋) = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)
43	1, 8, 10, 19, 21, 20, 29, 30, 42	invcoisoid 17790	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(⟨𝑋, 𝑌⟩ · 𝑋)𝐹) = ((Id‘𝐶)‘𝑋))
44	43	oveq2d 7415	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → (𝐺(⟨𝑋, 𝑋⟩ · 𝑍)(((𝑋(Inv‘𝐶)𝑌)‘𝐹)(⟨𝑋, 𝑌⟩ · 𝑋)𝐹)) = (𝐺(⟨𝑋, 𝑋⟩ · 𝑍)((Id‘𝐶)‘𝑋)))
45	1, 2, 30, 19, 21, 3, 26, 40	catrid 17681	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → (𝐺(⟨𝑋, 𝑋⟩ · 𝑍)((Id‘𝐶)‘𝑋)) = 𝐺)
46	41, 44, 45	3eqtrd 2773	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → ((𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = 𝐺)
47	46	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) ∧ 𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))) → ((𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) = 𝐺)
48	39, 47	eqtr2d 2770	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) ∧ 𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))) → 𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
49	37, 48	impbida 800	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑌𝐻𝑍)) → (𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ↔ 𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))))
50	49	ralrimiva 3130	. 2 ⊢ (𝜑 → ∀𝑘 ∈ (𝑌𝐻𝑍)(𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ↔ 𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹))))
51		reu6i 3709	. 2 ⊢ (((𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) ∈ (𝑌𝐻𝑍) ∧ ∀𝑘 ∈ (𝑌𝐻𝑍)(𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹) ↔ 𝑘 = (𝐺(⟨𝑌, 𝑋⟩ · 𝑍)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))) → ∃!𝑘 ∈ (𝑌𝐻𝑍)𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))
52	16, 50, 51	syl2anc 584	1 ⊢ (𝜑 → ∃!𝑘 ∈ (𝑌𝐻𝑍)𝐺 = (𝑘(⟨𝑋, 𝑌⟩ · 𝑍)𝐹))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ∃!wreu 3355  ⟨cop 4605  ‘cfv 6527  (class class class)co 7399  Basecbs 17213  Hom chom 17267  compcco 17268  Catccat 17661  Idccid 17662  Invcinv 17743  Isociso 17744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7356  df-ov 7402  df-oprab 7403  df-mpo 7404  df-1st 7982  df-2nd 7983  df-cat 17665  df-cid 17666  df-sect 17745  df-inv 17746  df-iso 17747

This theorem is referenced by:  upeu2  48928