Theorem isarep2

Description: Part of a study of the Axiom of Replacement used by the Isabelle prover. In Isabelle, the sethood of PrimReplace is apparently postulated implicitly by its type signature " [ i, [ i, i ] => o ] => i", which automatically asserts that it is a set without using any axioms. To prove that it is a set in Metamath, we need the hypotheses of Isabelle's "Axiom of Replacement" as well as the Axiom of Replacement in the form funimaex . (Contributed by NM, 26-Oct-2006)

	Ref	Expression
Hypotheses	isarep2.1	|- A e. _V
	isarep2.2	|- A. x e. A A. y A. z ( ( ph /\ [ z / y ] ph ) -> y = z )
Assertion	isarep2	|- E. w w = ( { <. x , y >. | ph } " A )

Proof

Step	Hyp	Ref	Expression
1		isarep2.1	|- A e. _V
2		isarep2.2	|- A. x e. A A. y A. z ( ( ph /\ [ z / y ] ph ) -> y = z )
3		resima	|- ( ( { <. x , y >. | ph } |` A ) " A ) = ( { <. x , y >. | ph } " A )
4		resopab	|- ( { <. x , y >. | ph } |` A ) = { <. x , y >. | ( x e. A /\ ph ) }
5	4	imaeq1i	|- ( ( { <. x , y >. | ph } |` A ) " A ) = ( { <. x , y >. | ( x e. A /\ ph ) } " A )
6	3 5	eqtr3i	|- ( { <. x , y >. | ph } " A ) = ( { <. x , y >. | ( x e. A /\ ph ) } " A )
7		funopab	|- ( Fun { <. x , y >. | ( x e. A /\ ph ) } <-> A. x E* y ( x e. A /\ ph ) )
8	2	rspec	|- ( x e. A -> A. y A. z ( ( ph /\ [ z / y ] ph ) -> y = z ) )
9		nfv	|- F/ z ph
10	9	mo3	|- ( E* y ph <-> A. y A. z ( ( ph /\ [ z / y ] ph ) -> y = z ) )
11	8 10	sylibr	|- ( x e. A -> E* y ph )
12		moanimv	|- ( E* y ( x e. A /\ ph ) <-> ( x e. A -> E* y ph ) )
13	11 12	mpbir	|- E* y ( x e. A /\ ph )
14	7 13	mpgbir	|- Fun { <. x , y >. | ( x e. A /\ ph ) }
15	1	funimaex	|- ( Fun { <. x , y >. | ( x e. A /\ ph ) } -> ( { <. x , y >. | ( x e. A /\ ph ) } " A ) e. _V )
16	14 15	ax-mp	|- ( { <. x , y >. | ( x e. A /\ ph ) } " A ) e. _V
17	6 16	eqeltri	|- ( { <. x , y >. | ph } " A ) e. _V
18	17	isseti	|- E. w w = ( { <. x , y >. | ph } " A )