This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )