oppcup3lem

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

Proof

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

Metamath Proof Explorer

Theorem oppcup3lem

Proof