funcsetcestrclem5

	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	funcsetcestrclem5	$⊢ (φ \land (X \in C \land Y \in C)) \to X G Y = {I ↾}_{(Y^{X})}$

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	6	adantr	$⊢ (φ \land (X \in C \land Y \in C)) \to G = (x \in C, y \in C ⟼ {I ↾}_{(y^{x})})$
8		oveq12	$⊢ (y = Y \land x = X) \to y^{x} = Y^{X}$
9	8	ancoms	$⊢ (x = X \land y = Y) \to y^{x} = Y^{X}$
10	9	reseq2d	$⊢ (x = X \land y = Y) \to {I ↾}_{(y^{x})} = {I ↾}_{(Y^{X})}$
11	10	adantl	$⊢ ((φ \land (X \in C \land Y \in C)) \land (x = X \land y = Y)) \to {I ↾}_{(y^{x})} = {I ↾}_{(Y^{X})}$
12		simprl	$⊢ (φ \land (X \in C \land Y \in C)) \to X \in C$
13		simprr	$⊢ (φ \land (X \in C \land Y \in C)) \to Y \in C$
14		ovexd	$⊢ (φ \land (X \in C \land Y \in C)) \to Y^{X} \in V$
15	14	resiexd	$⊢ (φ \land (X \in C \land Y \in C)) \to {I ↾}_{(Y^{X})} \in V$
16	7 11 12 13 15	ovmpod	$⊢ (φ \land (X \in C \land Y \in C)) \to X G Y = {I ↾}_{(Y^{X})}$

Metamath Proof Explorer