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

Metamath Proof Explorer

Theorem scottexs

Description: Theorem scheme version of scottex . The collection of all x of minimum rank such that ph ( x ) is true, is a set. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion scottexs 
|- { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } e. _V

Proof

Step Hyp Ref Expression
1 nfcv 
 |-  F/_ z { x | ph }
2 nfab1 
 |-  F/_ x { x | ph }
3 nfv 
 |-  F/ x ( rank ` z ) C_ ( rank ` y )
4 2 3 nfralw 
 |-  F/ x A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y )
5 nfv 
 |-  F/ z A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y )
6 fveq2 
 |-  ( z = x -> ( rank ` z ) = ( rank ` x ) )
7 6 sseq1d 
 |-  ( z = x -> ( ( rank ` z ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` y ) ) )
8 7 ralbidv 
 |-  ( z = x -> ( A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y ) <-> A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) ) )
9 1 2 4 5 8 cbvrabw 
 |-  { z e. { x | ph } | A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y ) } = { x e. { x | ph } | A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) }
10 df-rab 
 |-  { x e. { x | ph } | A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) } = { x | ( x e. { x | ph } /\ A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) ) }
11 abid 
 |-  ( x e. { x | ph } <-> ph )
12 df-ral 
 |-  ( A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) <-> A. y ( y e. { x | ph } -> ( rank ` x ) C_ ( rank ` y ) ) )
13 df-sbc 
 |-  ( [. y / x ]. ph <-> y e. { x | ph } )
14 13 imbi1i 
 |-  ( ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) <-> ( y e. { x | ph } -> ( rank ` x ) C_ ( rank ` y ) ) )
15 14 albii 
 |-  ( A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. y ( y e. { x | ph } -> ( rank ` x ) C_ ( rank ` y ) ) )
16 12 15 bitr4i 
 |-  ( A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) <-> A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) )
17 11 16 anbi12i 
 |-  ( ( x e. { x | ph } /\ A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) ) <-> ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) )
18 17 abbii 
 |-  { x | ( x e. { x | ph } /\ A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) ) } = { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) }
19 9 10 18 3eqtri 
 |-  { z e. { x | ph } | A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y ) } = { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) }
20 scottex 
 |-  { z e. { x | ph } | A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y ) } e. _V
21 19 20 eqeltrri 
 |-  { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } e. _V