funcringcsetclem5ALTV

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

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

Step	Hyp	Ref	Expression
1		funcringcsetcALTV.r	$⊢ R = RingCatALTV (U)$
2		funcringcsetcALTV.s	$⊢ S = SetCat (U)$
3		funcringcsetcALTV.b	$⊢ B = {Base}_{R}$
4		funcringcsetcALTV.c	$⊢ C = {Base}_{S}$
5		funcringcsetcALTV.u	$⊢ φ \to U \in WUni$
6		funcringcsetcALTV.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcringcsetcALTV.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