funcringcsetcALTV2lem5

Description: Lemma 5 for funcringcsetcALTV2 . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
	funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
	funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
	funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
	funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
	funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcringcsetcALTV2.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
Assertion	funcringcsetcALTV2lem5	$⊢ (φ \land (X \in B \land Y \in B)) \to X G Y = {I ↾}_{(X RingHom Y)}$

Step	Hyp	Ref	Expression
1		funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
2		funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
3		funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
4		funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
5		funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
6		funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcringcsetcALTV2.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
8	7	adantr	$⊢ (φ \land (X \in B \land Y \in B)) \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
9		oveq12	$⊢ (x = X \land y = Y) \to x RingHom y = X RingHom Y$
10	9	adantl	$⊢ ((φ \land (X \in B \land Y \in B)) \land (x = X \land y = Y)) \to x RingHom y = X RingHom Y$
11	10	reseq2d	$⊢ ((φ \land (X \in B \land Y \in B)) \land (x = X \land y = Y)) \to {I ↾}_{(x RingHom y)} = {I ↾}_{(X RingHom Y)}$
12		simprl	$⊢ (φ \land (X \in B \land Y \in B)) \to X \in B$
13		simprr	$⊢ (φ \land (X \in B \land Y \in B)) \to Y \in B$
14		ovexd	$⊢ (φ \land (X \in B \land Y \in B)) \to X RingHom Y \in V$
15	14	resiexd	$⊢ (φ \land (X \in B \land Y \in B)) \to {I ↾}_{(X RingHom Y)} \in V$
16	8 11 12 13 15	ovmpod	$⊢ (φ \land (X \in B \land Y \in B)) \to X G Y = {I ↾}_{(X RingHom Y)}$

Metamath Proof Explorer