Theorem upeu2 48902

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 48886	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
7		upcic.z	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝐶)
8		upcic.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐷)
9	8, 2, 5	funcf1 17907	. . . . 5 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
10		upcic.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
11	9, 10	ffvelcdmd 7103	. . . 4 ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐶)
12		upcic.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
13	9, 12	ffvelcdmd 7103	. . . 4 ⊢ (𝜑 → (𝐹‘𝑌) ∈ 𝐶)
14		upcic.m	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐽(𝐹‘𝑋)))
15		upcic.h	. . . . . 6 ⊢ 𝐻 = (Hom ‘𝐷)
16	8, 15, 3, 5, 10, 12	funcf2 17909	. . . . 5 ⊢ (𝜑 → (𝑋𝐺𝑌):(𝑋𝐻𝑌)⟶((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
17		upeu2.i	. . . . . . 7 ⊢ 𝐼 = (Iso‘𝐷)
18	5	funcrcl2 48885	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ Cat)
19	8, 15, 17, 18, 10, 12	isohom 17816	. . . . . 6 ⊢ (𝜑 → (𝑋𝐼𝑌) ⊆ (𝑋𝐻𝑌))
20		upeu2.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐼𝑌))
21	19, 20	sseldd 3983	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (𝑋𝐻𝑌))
22	16, 21	ffvelcdmd 7103	. . . 4 ⊢ (𝜑 → ((𝑋𝐺𝑌)‘𝐾) ∈ ((𝐹‘𝑋)𝐽(𝐹‘𝑌)))
23	2, 3, 4, 6, 7, 11, 13, 14, 22	catcocl 17724	. . 3 ⊢ (𝜑 → (((𝑋𝐺𝑌)‘𝐾)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑌))𝑀) ∈ (𝑍𝐽(𝐹‘𝑌)))
24	1, 23	eqeltrd 2840	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)))
25		upcic.1	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))
26	25	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → ∀𝑤 ∈ 𝐵 ∀𝑓 ∈ (𝑍𝐽(𝐹‘𝑤))∃!𝑘 ∈ (𝑋𝐻𝑤)𝑓 = (((𝑋𝐺𝑤)‘𝑘)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑤))𝑀))
27		simprl 771	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → 𝑣 ∈ 𝐵)
28		simprr 773	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))
29	26, 27, 28	upciclem1 48896	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → ∃!𝑝 ∈ (𝑋𝐻𝑣)𝑔 = (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀))
30		eqid 2736	. . . . . 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 17724	. . . . 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 48884	. . . . 5 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ 𝑝 ∈ (𝑋𝐻𝑣)) → ∃!𝑙 ∈ (𝑌𝐻𝑣)𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))
45		simprr 773	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))
46	45	fveq2d 6908	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → ((𝑋𝐺𝑣)‘𝑝) = ((𝑋𝐺𝑣)‘(𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾)))
47	46	oveq1d 7444	. . . . . . 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 771	. . . . . . . 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 48897	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → (((𝑋𝐺𝑣)‘(𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
58	47, 57	eqtrd 2776	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
59	58	eqeq2d 2747	. . . . 5 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) ∧ (𝑙 ∈ (𝑌𝐻𝑣) ∧ 𝑝 = (𝑙(⟨𝑋, 𝑌⟩(comp‘𝐷)𝑣)𝐾))) → (𝑔 = (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) ↔ 𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))
60	37, 44, 59	reuxfr1dd 48699	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → (∃!𝑝 ∈ (𝑋𝐻𝑣)𝑔 = (((𝑋𝐺𝑣)‘𝑝)(⟨𝑍, (𝐹‘𝑋)⟩𝑂(𝐹‘𝑣))𝑀) ↔ ∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))
61	29, 60	mpbid 232	. . 3 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑔 ∈ (𝑍𝐽(𝐹‘𝑣)))) → ∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
62	61	ralrimivva 3201	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁))
63	24, 62	jca 511	1 ⊢ (𝜑 → (𝑁 ∈ (𝑍𝐽(𝐹‘𝑌)) ∧ ∀𝑣 ∈ 𝐵 ∀𝑔 ∈ (𝑍𝐽(𝐹‘𝑣))∃!𝑙 ∈ (𝑌𝐻𝑣)𝑔 = (((𝑌𝐺𝑣)‘𝑙)(⟨𝑍, (𝐹‘𝑌)⟩𝑂(𝐹‘𝑣))𝑁)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3060  ∃!wreu 3377  ⟨cop 4630   class class class wbr 5141  ‘cfv 6559  (class class class)co 7429  Basecbs 17243  Hom chom 17304  compcco 17305  Catccat 17703  Isociso 17786   Func cfunc 17895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-1st 8010  df-2nd 8011  df-map 8864  df-ixp 8934  df-cat 17707  df-cid 17708  df-sect 17787  df-inv 17788  df-iso 17789  df-func 17899

This theorem is referenced by:  upeu4  48920