upciclem1

Description: Lemma for upcic , upeu , and upeu2 . (Contributed by Zhi Wang, 16-Sep-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	6	oveq2d	$⊢ y = Y \to ⟨Z, F (X)⟩ O F (y) = ⟨Z, F (X)⟩ O F (Y)$
9		oveq2	$⊢ y = Y \to X G y = X G Y$
10	9	fveq1d	$⊢ y = Y \to (X G y) (k) = (X G Y) (k)$
11		eqidd	$⊢ y = Y \to M = M$
12	8 10 11	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$
13	12	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)$
14	13	reubidv	$⊢ 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)$
15		oveq2	$⊢ y = Y \to X H y = X H Y$
16	15	reueqdv	$⊢ 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)$
17	14 16	bitrd	$⊢ 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)$
18	7 17	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)$
19	18 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$
20	5 19 3	rspcdva	$⊢ φ \to \exists! k \in (X H Y) N = (X G Y) (k) (⟨Z, F (X)⟩ O F (Y)) M$
21		fveq2	$⊢ k = m \to (X G Y) (k) = (X G Y) (m)$
22	21	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$
23	22	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)$
24	23	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$
25		fveq2	$⊢ m = l \to (X G Y) (m) = (X G Y) (l)$
26	25	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$
27	26	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)$
28	27	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$
29	24 28	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$
30	20 29	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