funcsetcestrclem6

	Ref	Expression
Hypotheses	funcsetcestrc.s	$⊢ S = SetCat (U)$
	funcsetcestrc.c	$⊢ C = {Base}_{S}$
	funcsetcestrc.f	$⊢ φ \to F = (x \in C ⟼ \{⟨{Base}_{ndx}, x⟩\})$
	funcsetcestrc.u	$⊢ φ \to U \in WUni$
	funcsetcestrc.o	$⊢ φ \to ω \in U$
	funcsetcestrc.g	$⊢ φ \to G = (x \in C, y \in C ⟼ {I ↾}_{(y^{x})})$
Assertion	funcsetcestrclem6	$⊢ (φ \land (X \in C \land Y \in C) \land H \in (Y^{X})) \to (X G Y) (H) = H$

Step	Hyp	Ref	Expression
1		funcsetcestrc.s	$⊢ S = SetCat (U)$
2		funcsetcestrc.c	$⊢ C = {Base}_{S}$
3		funcsetcestrc.f	$⊢ φ \to F = (x \in C ⟼ \{⟨{Base}_{ndx}, x⟩\})$
4		funcsetcestrc.u	$⊢ φ \to U \in WUni$
5		funcsetcestrc.o	$⊢ φ \to ω \in U$
6		funcsetcestrc.g	$⊢ φ \to G = (x \in C, y \in C ⟼ {I ↾}_{(y^{x})})$
7	1 2 3 4 5 6	funcsetcestrclem5	$⊢ (φ \land (X \in C \land Y \in C)) \to X G Y = {I ↾}_{(Y^{X})}$
8	7	3adant3	$⊢ (φ \land (X \in C \land Y \in C) \land H \in (Y^{X})) \to X G Y = {I ↾}_{(Y^{X})}$
9	8	fveq1d	$⊢ (φ \land (X \in C \land Y \in C) \land H \in (Y^{X})) \to (X G Y) (H) = ({I ↾}_{(Y^{X})}) (H)$
10		fvresi	$⊢ H \in (Y^{X}) \to ({I ↾}_{(Y^{X})}) (H) = H$
11	10	3ad2ant3	$⊢ (φ \land (X \in C \land Y \in C) \land H \in (Y^{X})) \to ({I ↾}_{(Y^{X})}) (H) = H$
12	9 11	eqtrd	$⊢ (φ \land (X \in C \land Y \in C) \land H \in (Y^{X})) \to (X G Y) (H) = H$

Metamath Proof Explorer