upciclem4

Description: Lemma for upcic and upeu . (Contributed by Zhi Wang, 19-Sep-2025)

	Ref	Expression
Hypotheses	upcic.b	$⊢ B = {Base}_{D}$
	upcic.c	$⊢ C = {Base}_{E}$
	upcic.h	$⊢ H = Hom (D)$
	upcic.j	$⊢ J = Hom (E)$
	upcic.o	$⊢ O = comp (E)$
	upcic.f	$⊢ φ \to F (D Func E) G$
	upcic.x	$⊢ φ \to X \in B$
	upcic.y	$⊢ φ \to Y \in B$
	upcic.z	$⊢ φ \to Z \in C$
	upcic.m	$⊢ φ \to M \in (Z J F (X))$
	upcic.1	$⊢ φ \to \forall w \in B \forall f \in (Z J F (w)) \exists! k \in (X H w) f = (X G w) (k) (⟨Z, F (X)⟩ O F (w)) M$
	upcic.n	$⊢ φ \to N \in (Z J F (Y))$
	upcic.2	$⊢ φ \to \forall v \in B \forall g \in (Z J F (v)) \exists! l \in (Y H v) g = (Y G v) (l) (⟨Z, F (Y)⟩ O F (v)) N$
Assertion	upciclem4	$⊢ φ \to (X ≃_{𝑐} (D) Y \land \exists r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M)$

Proof

Step	Hyp	Ref	Expression
1		upcic.b	$⊢ B = {Base}_{D}$
2		upcic.c	$⊢ C = {Base}_{E}$
3		upcic.h	$⊢ H = Hom (D)$
4		upcic.j	$⊢ J = Hom (E)$
5		upcic.o	$⊢ O = comp (E)$
6		upcic.f	$⊢ φ \to F (D Func E) G$
7		upcic.x	$⊢ φ \to X \in B$
8		upcic.y	$⊢ φ \to Y \in B$
9		upcic.z	$⊢ φ \to Z \in C$
10		upcic.m	$⊢ φ \to M \in (Z J F (X))$
11		upcic.1	$⊢ φ \to \forall w \in B \forall f \in (Z J F (w)) \exists! k \in (X H w) f = (X G w) (k) (⟨Z, F (X)⟩ O F (w)) M$
12		upcic.n	$⊢ φ \to N \in (Z J F (Y))$
13		upcic.2	$⊢ φ \to \forall v \in B \forall g \in (Z J F (v)) \exists! l \in (Y H v) g = (Y G v) (l) (⟨Z, F (Y)⟩ O F (v)) N$
14	11 8 12	upciclem1	$⊢ φ \to \exists! p \in (X H Y) N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M$
15		reurex	$⊢ \exists! p \in (X H Y) N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M \to \exists p \in (X H Y) N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M$
16	14 15	syl	$⊢ φ \to \exists p \in (X H Y) N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M$
17		simpl	$⊢ (φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \to φ$
18	13 7 10	upciclem1	$⊢ φ \to \exists! q \in (Y H X) M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N$
19		reurex	$⊢ \exists! q \in (Y H X) M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N \to \exists q \in (Y H X) M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N$
20	17 18 19	3syl	$⊢ (φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \to \exists q \in (Y H X) M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N$
21		eqid	$⊢ Iso (D) = Iso (D)$
22	6	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to F (D Func E) G$
23	22	funcrcl2	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to D \in Cat$
24	7	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to X \in B$
25	8	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to Y \in B$
26		eqid	$⊢ comp (D) = comp (D)$
27		eqid	$⊢ Id (D) = Id (D)$
28		simplrl	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to p \in (X H Y)$
29		simprl	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to q \in (Y H X)$
30	9	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to Z \in C$
31	10	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to M \in (Z J F (X))$
32	11	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to \forall w \in B \forall f \in (Z J F (w)) \exists! k \in (X H w) f = (X G w) (k) (⟨Z, F (X)⟩ O F (w)) M$
33		simprr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N$
34		simplrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M$
35	1 2 3 4 5 22 24 25 30 31 32 26 28 29 33 34	upciclem3	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to q (⟨X, Y⟩ comp (D) X) p = Id (D) (X)$
36	12	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to N \in (Z J F (Y))$
37	13	ad2antrr	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to \forall v \in B \forall g \in (Z J F (v)) \exists! l \in (Y H v) g = (Y G v) (l) (⟨Z, F (Y)⟩ O F (v)) N$
38	1 2 3 4 5 22 25 24 30 36 37 26 29 28 34 33	upciclem3	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to p (⟨Y, X⟩ comp (D) Y) q = Id (D) (Y)$
39	1 3 26 21 27 23 24 25 28 29 35 38	isisod	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to p \in (X Iso (D) Y)$
40	21 1 23 24 25 39	brcici	$⊢ ((φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \land (q \in (Y H X) \land M = (Y G X) (q) (⟨Z, F (Y)⟩ O F (X)) N)) \to X ≃_{𝑐} (D) Y$
41	20 40	rexlimddv	$⊢ (φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \to X ≃_{𝑐} (D) Y$
42	16 41	rexlimddv	$⊢ φ \to X ≃_{𝑐} (D) Y$
43	20 39	rexlimddv	$⊢ (φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \to p \in (X Iso (D) Y)$
44		simprr	$⊢ (φ \land (p \in (X H Y) \land N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M)) \to N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M$
45	16 43 44	reximssdv	$⊢ φ \to \exists p \in (X Iso (D) Y) N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M$
46		fveq2	$⊢ p = r \to (X G Y) (p) = (X G Y) (r)$
47	46	oveq1d	$⊢ p = r \to (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
48	47	eqeq2d	$⊢ p = r \to (N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M)$
49	48	cbvrexvw	$⊢ \exists p \in (X Iso (D) Y) N = (X G Y) (p) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow \exists r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
50	45 49	sylib	$⊢ φ \to \exists r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
51	42 50	jca	$⊢ φ \to (X ≃_{𝑐} (D) Y \land \exists r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M)$

Metamath Proof Explorer

Theorem upciclem4

Proof