funcringcsetcALTV2lem6

Description: Lemma 6 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	funcringcsetcALTV2lem6	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = H$

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	1 2 3 4 5 6 7	funcringcsetcALTV2lem5	$⊢ (φ \land (X \in B \land Y \in B)) \to X G Y = {I ↾}_{(X RingHom Y)}$
9	8	3adant3	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to X G Y = {I ↾}_{(X RingHom Y)}$
10	9	fveq1d	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = ({I ↾}_{(X RingHom Y)}) (H)$
11		fvresi	$⊢ H \in (X RingHom Y) \to ({I ↾}_{(X RingHom Y)}) (H) = H$
12	11	3ad2ant3	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to ({I ↾}_{(X RingHom Y)}) (H) = H$
13	10 12	eqtrd	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = H$

Metamath Proof Explorer