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 abeq2i
 |-  ( 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 syl6bir
 |-  ( 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 )