upciclem1

Description: Lemma for upcic , upeu , and upeu2 . (Contributed by Zhi Wang, 16-Sep-2025) (Proof shortened by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	upciclem1.1	$⊢ φ \to \forall y \in B \forall n \in (Z J F (y)) \exists! k \in (X H y) n = (X G y) (k) (⟨Z, F (X)⟩ O F (y)) M$
	upciclem1.y	$⊢ φ \to Y \in B$
	upciclem1.n	$⊢ φ \to N \in (Z J F (Y))$
Assertion	upciclem1	$⊢ φ \to \exists! l \in (X H Y) N = (X G Y) (l) (⟨Z, F (X)⟩ O F (Y)) M$

Proof

Step	Hyp	Ref	Expression
1		upciclem1.1	$⊢ φ \to \forall y \in B \forall n \in (Z J F (y)) \exists! k \in (X H y) n = (X G y) (k) (⟨Z, F (X)⟩ O F (y)) M$
2		upciclem1.y	$⊢ φ \to Y \in B$
3		upciclem1.n	$⊢ φ \to N \in (Z J F (Y))$
4		eqeq1	$⊢ n = N \to (n = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow N = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M)$
5	4	reubidv	$⊢ n = N \to (\exists! k \in (X H Y) n = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow \exists! k \in (X H Y) N = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M)$
6		fveq2	$⊢ y = Y \to F (y) = F (Y)$
7	6	oveq2d	$⊢ y = Y \to Z J F (y) = Z J F (Y)$
8		oveq2	$⊢ y = Y \to X H y = X H Y$
9	6	oveq2d	$⊢ y = Y \to ⟨Z, F (X)⟩ O F (y) = ⟨Z, F (X)⟩ O F (Y)$
10		oveq2	$⊢ y = Y \to X G y = X G Y$
11	10	fveq1d	$⊢ y = Y \to (X G y) (k) = (X G Y) (k)$
12		eqidd	$⊢ y = Y \to M = M$
13	9 11 12	oveq123d	$⊢ y = Y \to (X G y) (k) (⟨Z, F (X)⟩ O F (y)) M = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M$
14	13	eqeq2d	$⊢ y = Y \to (n = (X G y) (k) (⟨Z, F (X)⟩ O F (y)) M \leftrightarrow n = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M)$
15	8 14	reueqbidv	$⊢ y = Y \to (\exists! k \in (X H y) n = (X G y) (k) (⟨Z, F (X)⟩ O F (y)) M \leftrightarrow \exists! k \in (X H Y) n = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M)$
16	7 15	raleqbidv	$⊢ y = Y \to (\forall n \in (Z J F (y)) \exists! k \in (X H y) n = (X G y) (k) (⟨Z, F (X)⟩ O F (y)) M \leftrightarrow \forall n \in (Z J F (Y)) \exists! k \in (X H Y) n = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M)$
17	16 1 2	rspcdva	$⊢ φ \to \forall n \in (Z J F (Y)) \exists! k \in (X H Y) n = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M$
18	5 17 3	rspcdva	$⊢ φ \to \exists! k \in (X H Y) N = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M$
19		fveq2	$⊢ k = m \to (X G Y) (k) = (X G Y) (m)$
20	19	oveq1d	$⊢ k = m \to (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M = (X G Y) (m) (⟨Z, F (X)⟩ O F (Y)) M$
21	20	eqeq2d	$⊢ k = m \to (N = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow N = (X G Y) (m) (⟨Z, F (X)⟩ O F (Y)) M)$
22	21	cbvreuvw	$⊢ \exists! k \in (X H Y) N = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow \exists! m \in (X H Y) N = (X G Y) (m) (⟨Z, F (X)⟩ O F (Y)) M$
23		fveq2	$⊢ m = l \to (X G Y) (m) = (X G Y) (l)$
24	23	oveq1d	$⊢ m = l \to (X G Y) (m) (⟨Z, F (X)⟩ O F (Y)) M = (X G Y) (l) (⟨Z, F (X)⟩ O F (Y)) M$
25	24	eqeq2d	$⊢ m = l \to (N = (X G Y) (m) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow N = (X G Y) (l) (⟨Z, F (X)⟩ O F (Y)) M)$
26	25	cbvreuvw	$⊢ \exists! m \in (X H Y) N = (X G Y) (m) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow \exists! l \in (X H Y) N = (X G Y) (l) (⟨Z, F (X)⟩ O F (Y)) M$
27	22 26	bitri	$⊢ \exists! k \in (X H Y) N = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow \exists! l \in (X H Y) N = (X G Y) (l) (⟨Z, F (X)⟩ O F (Y)) M$
28	18 27	sylib	$⊢ φ \to \exists! l \in (X H Y) N = (X G Y) (l) (⟨Z, F (X)⟩ O F (Y)) M$

Metamath Proof Explorer

Theorem upciclem1

Proof