Metamath Proof Explorer

Theorem scott0s

Description: Theorem scheme version of scott0 . The collection of all x of minimum rank such that ph ( x ) is true, is not empty iff there is an x such that ph ( x ) holds. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion scott0s 
|- ( E. x ph <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } =/= (/) )

Proof

Step Hyp Ref Expression
1 abn0 
 |-  ( { x | ph } =/= (/) <-> E. x ph )
2 scott0 
 |-  ( { x | ph } = (/) <-> { z e. { x | ph } | A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y ) } = (/) )
3 nfcv 
 |-  F/_ z { x | ph }
4 nfab1 
 |-  F/_ x { x | ph }
5 nfv 
 |-  F/ x ( rank ` z ) C_ ( rank ` y )
6 4 5 nfralw 
 |-  F/ x A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y )
7 nfv 
 |-  F/ z A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y )
8 fveq2 
 |-  ( z = x -> ( rank ` z ) = ( rank ` x ) )
9 8 sseq1d 
 |-  ( z = x -> ( ( rank ` z ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` y ) ) )
10 9 ralbidv 
 |-  ( z = x -> ( A. y e. { x | ph } ( rank ` z ) C_ ( rank ` y ) <-> A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) ) )
11 3 4 6 7 10 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 ) }
12 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 ) ) }
13 abid 
 |-  ( x e. { x | ph } <-> ph )
14 df-ral 
 |-  ( A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) <-> A. y ( y e. { x | ph } -> ( rank ` x ) C_ ( rank ` y ) ) )
15 df-sbc 
 |-  ( [. y / x ]. ph <-> y e. { x | ph } )
16 15 imbi1i 
 |-  ( ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) <-> ( y e. { x | ph } -> ( rank ` x ) C_ ( rank ` y ) ) )
17 16 albii 
 |-  ( A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. y ( y e. { x | ph } -> ( rank ` x ) C_ ( rank ` y ) ) )
18 14 17 bitr4i 
 |-  ( A. y e. { x | ph } ( rank ` x ) C_ ( rank ` y ) <-> A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) )
19 13 18 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 ) ) ) )
20 19 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 ) ) ) }
21 11 12 20 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 ) ) ) }
22 21 eqeq1i 
 |-  ( { 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 ) ) ) } = (/) )
23 2 22 bitri 
 |-  ( { x | ph } = (/) <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } = (/) )
24 23 necon3bii 
 |-  ( { x | ph } =/= (/) <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } =/= (/) )
25 1 24 bitr3i 
 |-  ( E. x ph <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } =/= (/) )