funcsetcestrclem4

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		eqid	$⊢ (x \in C, y \in C ⟼ {I ↾}_{(y^{x})}) = (x \in C, y \in C ⟼ {I ↾}_{(y^{x})})$
8		ovex	$⊢ y^{x} \in V$
9		resiexg	$⊢ y^{x} \in V \to {I ↾}_{(y^{x})} \in V$
10	8 9	ax-mp	$⊢ {I ↾}_{(y^{x})} \in V$
11	7 10	fnmpoi	$⊢ (x \in C, y \in C ⟼ {I ↾}_{(y^{x})}) Fn (C \times C)$
12	6	fneq1d	$⊢ φ \to (G Fn (C \times C) \leftrightarrow (x \in C, y \in C ⟼ {I ↾}_{(y^{x})}) Fn (C \times C))$
13	11 12	mpbiri	$⊢ φ \to G Fn (C \times C)$

Metamath Proof Explorer