funcestrcsetclem6

	Ref	Expression
Hypotheses	funcestrcsetc.e	$⊢ E = ExtStrCat (U)$
	funcestrcsetc.s	$⊢ S = SetCat (U)$
	funcestrcsetc.b	$⊢ B = {Base}_{E}$
	funcestrcsetc.c	$⊢ C = {Base}_{S}$
	funcestrcsetc.u	$⊢ φ \to U \in WUni$
	funcestrcsetc.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcestrcsetc.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{({Base}_{y}^{{Base}_{x}})})$
	funcestrcsetc.m	$⊢ M = {Base}_{X}$
	funcestrcsetc.n	$⊢ N = {Base}_{Y}$
Assertion	funcestrcsetclem6	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (N^{M})) \to (X G Y) (H) = H$

Step	Hyp	Ref	Expression
1		funcestrcsetc.e	$⊢ E = ExtStrCat (U)$
2		funcestrcsetc.s	$⊢ S = SetCat (U)$
3		funcestrcsetc.b	$⊢ B = {Base}_{E}$
4		funcestrcsetc.c	$⊢ C = {Base}_{S}$
5		funcestrcsetc.u	$⊢ φ \to U \in WUni$
6		funcestrcsetc.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcestrcsetc.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{({Base}_{y}^{{Base}_{x}})})$
8		funcestrcsetc.m	$⊢ M = {Base}_{X}$
9		funcestrcsetc.n	$⊢ N = {Base}_{Y}$
10	1 2 3 4 5 6 7 8 9	funcestrcsetclem5	$⊢ (φ \land (X \in B \land Y \in B)) \to X G Y = {I ↾}_{(N^{M})}$
11	10	3adant3	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (N^{M})) \to X G Y = {I ↾}_{(N^{M})}$
12	11	fveq1d	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (N^{M})) \to (X G Y) (H) = ({I ↾}_{(N^{M})}) (H)$
13		fvresi	$⊢ H \in (N^{M}) \to ({I ↾}_{(N^{M})}) (H) = H$
14	13	3ad2ant3	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (N^{M})) \to ({I ↾}_{(N^{M})}) (H) = H$
15	12 14	eqtrd	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (N^{M})) \to (X G Y) (H) = H$

Metamath Proof Explorer