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

Metamath Proof Explorer

Theorem cp

Description: Collection Principle. This remarkable theorem scheme is in effect a very strong generalization of the Axiom of Replacement. The proof makes use of Scott's trick scottex that collapses a proper class into a set of minimum rank. The wff ph can be thought of as ph ( x , y ) . Scheme "Collection Principle" of Jech p. 72. (Contributed by NM, 17-Oct-2003)

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

Proof

Step Hyp Ref Expression
1 vex 
 |-  z e. _V
2 1 cplem2 
 |-  E. w A. x e. z ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) )
3 abn0 
 |-  ( { y | ph } =/= (/) <-> E. y ph )
4 elin 
 |-  ( y e. ( { y | ph } i^i w ) <-> ( y e. { y | ph } /\ y e. w ) )
5 abid 
 |-  ( y e. { y | ph } <-> ph )
6 5 anbi1i 
 |-  ( ( y e. { y | ph } /\ y e. w ) <-> ( ph /\ y e. w ) )
7 ancom 
 |-  ( ( ph /\ y e. w ) <-> ( y e. w /\ ph ) )
8 4 6 7 3bitri 
 |-  ( y e. ( { y | ph } i^i w ) <-> ( y e. w /\ ph ) )
9 8 exbii 
 |-  ( E. y y e. ( { y | ph } i^i w ) <-> E. y ( y e. w /\ ph ) )
10 nfab1 
 |-  F/_ y { y | ph }
11 nfcv 
 |-  F/_ y w
12 10 11 nfin 
 |-  F/_ y ( { y | ph } i^i w )
13 12 n0f 
 |-  ( ( { y | ph } i^i w ) =/= (/) <-> E. y y e. ( { y | ph } i^i w ) )
14 df-rex 
 |-  ( E. y e. w ph <-> E. y ( y e. w /\ ph ) )
15 9 13 14 3bitr4i 
 |-  ( ( { y | ph } i^i w ) =/= (/) <-> E. y e. w ph )
16 3 15 imbi12i 
 |-  ( ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) ) <-> ( E. y ph -> E. y e. w ph ) )
17 16 ralbii 
 |-  ( A. x e. z ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) ) <-> A. x e. z ( E. y ph -> E. y e. w ph ) )
18 17 exbii 
 |-  ( E. w A. x e. z ( { y | ph } =/= (/) -> ( { y | ph } i^i w ) =/= (/) ) <-> E. w A. x e. z ( E. y ph -> E. y e. w ph ) )
19 2 18 mpbi 
 |-  E. w A. x e. z ( E. y ph -> E. y e. w ph )