Theorem upeu2 48956

Description: Generate new universal morphism through isomorphism from existing universal object. (Contributed by Zhi Wang, 20-Sep-2025.)

Hypotheses

Ref	Expression
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	⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))
upeu2.i	⊢ 𝐼 = (Iso‘𝐷)
upeu2.k	⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌))
upeu2.n	⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))

Assertion

Ref	Expression
upeu2	⊢ (𝜑 → (𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)) ∧ ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))

Distinct variable groups:   𝐵,𝑔,𝑙   𝑤,𝐵   𝐷,𝑙   𝑓,𝐹,𝑘,𝑤   𝐹,𝑙   𝑓,𝐺,𝑘,𝑤   𝐺,𝑙   𝑓,𝐻,𝑘,𝑤   𝐻,𝑙   𝑓,𝐽,𝑤   𝐽,𝑙   𝐾,𝑙   𝑓,𝑀,𝑘,𝑤   𝑀,𝑙   𝑓,𝑂,𝑘,𝑤   𝑂,𝑙   𝑓,𝑋,𝑘,𝑤   𝑋,𝑙   𝑌,𝑙   𝑓,𝑍,𝑘,𝑤   𝑍,𝑙   𝑓,𝑔,𝑣,𝑘   𝜑,𝑔,𝑙,𝑣   𝑤,𝑣

Allowed substitution hints:   𝜑(𝑤,𝑓,𝑘)   𝐵(𝑣,𝑓,𝑘)   𝐶(𝑤,𝑣,𝑓,𝑔,𝑘,𝑙)   𝐷(𝑤,𝑣,𝑓,𝑔,𝑘)   𝐸(𝑤,𝑣,𝑓,𝑔,𝑘,𝑙)   𝐹(𝑣,𝑔)   𝐺(𝑣,𝑔)   𝐻(𝑣,𝑔)   𝐼(𝑤,𝑣,𝑓,𝑔,𝑘,𝑙)   𝐽(𝑣,𝑔,𝑘)   𝐾(𝑤,𝑣,𝑓,𝑔,𝑘)   𝑀(𝑣,𝑔)   𝑁(𝑤,𝑣,𝑓,𝑔,𝑘,𝑙)   𝑂(𝑣,𝑔)   𝑋(𝑣,𝑔)   𝑌(𝑤,𝑣,𝑓,𝑔,𝑘)   𝑍(𝑣,𝑔)

Proof of Theorem upeu2

Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		upeu2.n	. . 3 ⊢ (𝜑 → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
2		upcic.c	. . . 4 ⊢ 𝐶 = (Base‘𝐸)
3		upcic.j	. . . 4 ⊢ 𝐽 = (Hom ‘𝐸)
4		upcic.o	. . . 4 ⊢ 𝑂 = (comp‘𝐸)
5		upcic.f	. . . . 5 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
6	5	funcrcl3 48938	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
7		upcic.z	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝐶)
8		upcic.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐷)
9	8, 2, 5	funcf1 17883	. . . . 5 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
10		upcic.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
11	9, 10	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐶)
12		upcic.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
13	9, 12	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝐶)
14		upcic.m	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))
15		upcic.h	. . . . . 6 ⊢ 𝐻 = (Hom ‘𝐷)
16	8, 15, 3, 5, 10, 12	funcf2 17885	. . . . 5 ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
17		upeu2.i	. . . . . . 7 ⊢ 𝐼 = (Iso‘𝐷)
18	5	funcrcl2 48937	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ Cat)
19	8, 15, 17, 18, 10, 12	isohom 17792	. . . . . 6 ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌))
20		upeu2.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌))
21	19, 20	sseldd 3964	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))
22	16, 21	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝐾) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
23	2, 3, 4, 6, 7, 11, 13, 14, 22	catcocl 17700	. . 3 ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀) ∈ (𝑍𝐽(𝐹‘𝑌)))
24	1, 23	eqeltrd 2833	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))
25		upcic.1	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))
26	25	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))
27		simprl 770	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → 𝑣 ∈ 𝐵)
28		simprr 772	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))
29	26, 27, 28	upciclem1 48950	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → ∃!𝑝 ∈ (𝑋𝐻𝑣)𝑔 = (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀))
30		eqid 2734	. . . . . 6 ⊢ (comp‘𝐷) = (comp‘𝐷)
31	18	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑙 ∈ (𝑌𝐻𝑣)) → 𝐷 ∈ Cat)
32	10	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑙 ∈ (𝑌𝐻𝑣)) → 𝑋 ∈ 𝐵)
33	12	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑙 ∈ (𝑌𝐻𝑣)) → 𝑌 ∈ 𝐵)
34	27	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑙 ∈ (𝑌𝐻𝑣)) → 𝑣 ∈ 𝐵)
35	21	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑙 ∈ (𝑌𝐻𝑣)) → 𝐾 ∈ (𝑋𝐻𝑌))
36		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑙 ∈ (𝑌𝐻𝑣)) → 𝑙 ∈ (𝑌𝐻𝑣))
37	8, 15, 30, 31, 32, 33, 34, 35, 36	catcocl 17700	. . . . 5 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑙 ∈ (𝑌𝐻𝑣)) → (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾) ∈ (𝑋𝐻𝑣))
38	18	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → 𝐷 ∈ Cat)
39	10	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → 𝑋 ∈ 𝐵)
40	12	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → 𝑌 ∈ 𝐵)
41	27	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → 𝑣 ∈ 𝐵)
42	20	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → 𝐾 ∈ (𝑋𝐼𝑌))
43		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → 𝑝 ∈ (𝑋𝐻𝑣))
44	8, 15, 30, 17, 38, 39, 40, 41, 42, 43	upeu2lem 48905	. . . . 5 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → ∃!𝑙 ∈ (𝑌𝐻𝑣)𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))
45		simprr 772	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))
46	45	fveq2d 6890	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → ((𝑋𝐺𝑣)‘𝑝) = ((𝑋𝐺𝑣)‘(𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾)))
47	46	oveq1d 7428	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) = (((𝑋𝐺𝑣)‘(𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀))
48	5	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝐹(𝐷 Func 𝐸)𝐺)
49	10	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑋 ∈ 𝐵)
50	12	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑌 ∈ 𝐵)
51	27	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑣 ∈ 𝐵)
52	7	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑍 ∈ 𝐶)
53	14	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))
54	21	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝐾 ∈ (𝑋𝐻𝑌))
55		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑙 ∈ (𝑌𝐻𝑣))
56	1	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑁 = (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀))
57	8, 2, 15, 3, 4, 48, 49, 50, 51, 52, 53, 30, 54, 55, 56	upciclem2 48951	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → (((𝑋𝐺𝑣)‘(𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
58	47, 57	eqtrd 2769	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
59	58	eqeq2d 2745	. . . . 5 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → (𝑔 = (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) ↔ 𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))
60	37, 44, 59	reuxfr1dd 48699	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → (∃!𝑝 ∈ (𝑋𝐻𝑣)𝑔 = (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) ↔ ∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))
61	29, 60	mpbid 232	. . 3 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → ∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
62	61	ralrimivva 3189	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
63	24, 62	jca 511	1 ⊢ (𝜑 → (𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)) ∧ ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ∃!wreu 3361  ⟨cop 4612   class class class wbr 5123  ‘cfv 6541  (class class class)co 7413  Basecbs 17230  Hom chom 17285  compcco 17286  Catccat 17679  Isociso 17762   Func cfunc 17871

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 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

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 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7996  df-2nd 7997  df-map 8850  df-ixp 8920  df-cat 17683  df-cid 17684  df-sect 17763  df-inv 17764  df-iso 17765  df-func 17875

This theorem is referenced by:  upeu4  48978