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

Metamath Proof Explorer

Theorem zfrep6

Description: A version of the Axiom of Replacement. Normally ph would have free variables x and y . Axiom 6 of Kunen p. 12. The Separation Scheme ax-sep cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep . (Contributed by NM, 10-Oct-2003)

Ref Expression
Assertion zfrep6 
|- ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )

Proof

Step Hyp Ref Expression
1 19.42v 
 |-  ( E. y ( x e. z /\ ph ) <-> ( x e. z /\ E. y ph ) )
2 1 abbii 
 |-  { x | E. y ( x e. z /\ ph ) } = { x | ( x e. z /\ E. y ph ) }
3 dmopab 
 |-  dom { <. x , y >. | ( x e. z /\ ph ) } = { x | E. y ( x e. z /\ ph ) }
4 df-rab 
 |-  { x e. z | E. y ph } = { x | ( x e. z /\ E. y ph ) }
5 2 3 4 3eqtr4i 
 |-  dom { <. x , y >. | ( x e. z /\ ph ) } = { x e. z | E. y ph }
6 euex 
 |-  ( E! y ph -> E. y ph )
7 6 ralimi 
 |-  ( A. x e. z E! y ph -> A. x e. z E. y ph )
8 rabid2 
 |-  ( z = { x e. z | E. y ph } <-> A. x e. z E. y ph )
9 7 8 sylibr 
 |-  ( A. x e. z E! y ph -> z = { x e. z | E. y ph } )
10 5 9 eqtr4id 
 |-  ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } = z )
11 vex 
 |-  z e. _V
12 10 11 eqeltrdi 
 |-  ( A. x e. z E! y ph -> dom { <. x , y >. | ( x e. z /\ ph ) } e. _V )
13 eumo 
 |-  ( E! y ph -> E* y ph )
14 13 imim2i 
 |-  ( ( x e. z -> E! y ph ) -> ( x e. z -> E* y ph ) )
15 moanimv 
 |-  ( E* y ( x e. z /\ ph ) <-> ( x e. z -> E* y ph ) )
16 14 15 sylibr 
 |-  ( ( x e. z -> E! y ph ) -> E* y ( x e. z /\ ph ) )
17 16 alimi 
 |-  ( A. x ( x e. z -> E! y ph ) -> A. x E* y ( x e. z /\ ph ) )
18 df-ral 
 |-  ( A. x e. z E! y ph <-> A. x ( x e. z -> E! y ph ) )
19 funopab 
 |-  ( Fun { <. x , y >. | ( x e. z /\ ph ) } <-> A. x E* y ( x e. z /\ ph ) )
20 17 18 19 3imtr4i 
 |-  ( A. x e. z E! y ph -> Fun { <. x , y >. | ( x e. z /\ ph ) } )
21 funrnex 
 |-  ( dom { <. x , y >. | ( x e. z /\ ph ) } e. _V -> ( Fun { <. x , y >. | ( x e. z /\ ph ) } -> ran { <. x , y >. | ( x e. z /\ ph ) } e. _V ) )
22 12 20 21 sylc 
 |-  ( A. x e. z E! y ph -> ran { <. x , y >. | ( x e. z /\ ph ) } e. _V )
23 nfra1 
 |-  F/ x A. x e. z E! y ph
24 10 eleq2d 
 |-  ( A. x e. z E! y ph -> ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> x e. z ) )
25 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } <-> ( x e. z /\ ph ) )
26 vex 
 |-  x e. _V
27 vex 
 |-  y e. _V
28 26 27 opelrn 
 |-  ( <. x , y >. e. { <. x , y >. | ( x e. z /\ ph ) } -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } )
29 25 28 sylbir 
 |-  ( ( x e. z /\ ph ) -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } )
30 29 ex 
 |-  ( x e. z -> ( ph -> y e. ran { <. x , y >. | ( x e. z /\ ph ) } ) )
31 30 impac 
 |-  ( ( x e. z /\ ph ) -> ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
32 31 eximi 
 |-  ( E. y ( x e. z /\ ph ) -> E. y ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
33 3 eqabri 
 |-  ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } <-> E. y ( x e. z /\ ph ) )
34 df-rex 
 |-  ( E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph <-> E. y ( y e. ran { <. x , y >. | ( x e. z /\ ph ) } /\ ph ) )
35 32 33 34 3imtr4i 
 |-  ( x e. dom { <. x , y >. | ( x e. z /\ ph ) } -> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph )
36 24 35 biimtrrdi 
 |-  ( A. x e. z E! y ph -> ( x e. z -> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) )
37 23 36 ralrimi 
 |-  ( A. x e. z E! y ph -> A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph )
38 nfopab1 
 |-  F/_ x { <. x , y >. | ( x e. z /\ ph ) }
39 38 nfrn 
 |-  F/_ x ran { <. x , y >. | ( x e. z /\ ph ) }
40 39 nfeq2 
 |-  F/ x w = ran { <. x , y >. | ( x e. z /\ ph ) }
41 nfcv 
 |-  F/_ y w
42 nfopab2 
 |-  F/_ y { <. x , y >. | ( x e. z /\ ph ) }
43 42 nfrn 
 |-  F/_ y ran { <. x , y >. | ( x e. z /\ ph ) }
44 41 43 rexeqf 
 |-  ( w = ran { <. x , y >. | ( x e. z /\ ph ) } -> ( E. y e. w ph <-> E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) )
45 40 44 ralbid 
 |-  ( w = ran { <. x , y >. | ( x e. z /\ ph ) } -> ( A. x e. z E. y e. w ph <-> A. x e. z E. y e. ran { <. x , y >. | ( x e. z /\ ph ) } ph ) )
46 22 37 45 spcedv 
 |-  ( A. x e. z E! y ph -> E. w A. x e. z E. y e. w ph )