Metamath Proof Explorer

Theorem scottabf

Description: Value of the Scott operation at a class abstraction. Variant of scottab with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023)

Ref Expression
Hypotheses scottabf.1 
|- F/ x ps
scottabf.2 
|- ( x = y -> ( ph <-> ps ) )
Assertion scottabf 
|- Scott { x | ph } = { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) }

Proof

Step Hyp Ref Expression
1 scottabf.1 
 |-  F/ x ps
2 scottabf.2 
 |-  ( x = y -> ( ph <-> ps ) )
3 df-scott 
 |-  Scott { x | ph } = { z e. { x | ph } | A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) }
4 df-rab 
 |-  { z e. { x | ph } | A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) } = { z | ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) }
5 abeq1 
 |-  ( { z | ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) } = { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) } <-> A. z ( ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) <-> z e. { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) } ) )
6 nfsab1 
 |-  F/ x z e. { x | ph }
7 nfab1 
 |-  F/_ x { x | ph }
8 nfv 
 |-  F/ x ( rank ` z ) C_ ( rank ` w )
9 7 8 nfralw 
 |-  F/ x A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w )
10 6 9 nfan 
 |-  F/ x ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) )
11 vex 
 |-  z e. _V
12 abid 
 |-  ( x e. { x | ph } <-> ph )
13 eleq1w 
 |-  ( x = z -> ( x e. { x | ph } <-> z e. { x | ph } ) )
14 12 13 bitr3id 
 |-  ( x = z -> ( ph <-> z e. { x | ph } ) )
15 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
16 1 2 sbiev 
 |-  ( [ y / x ] ph <-> ps )
17 15 16 bitr2i 
 |-  ( ps <-> y e. { x | ph } )
18 eleq1w 
 |-  ( y = w -> ( y e. { x | ph } <-> w e. { x | ph } ) )
19 17 18 syl5bb 
 |-  ( y = w -> ( ps <-> w e. { x | ph } ) )
20 19 adantl 
 |-  ( ( x = z /\ y = w ) -> ( ps <-> w e. { x | ph } ) )
21 simpl 
 |-  ( ( x = z /\ y = w ) -> x = z )
22 21 fveq2d 
 |-  ( ( x = z /\ y = w ) -> ( rank ` x ) = ( rank ` z ) )
23 simpr 
 |-  ( ( x = z /\ y = w ) -> y = w )
24 23 fveq2d 
 |-  ( ( x = z /\ y = w ) -> ( rank ` y ) = ( rank ` w ) )
25 22 24 sseq12d 
 |-  ( ( x = z /\ y = w ) -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` z ) C_ ( rank ` w ) ) )
26 20 25 imbi12d 
 |-  ( ( x = z /\ y = w ) -> ( ( ps -> ( rank ` x ) C_ ( rank ` y ) ) <-> ( w e. { x | ph } -> ( rank ` z ) C_ ( rank ` w ) ) ) )
27 26 cbvaldvaw 
 |-  ( x = z -> ( A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. w ( w e. { x | ph } -> ( rank ` z ) C_ ( rank ` w ) ) ) )
28 df-ral 
 |-  ( A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) <-> A. w ( w e. { x | ph } -> ( rank ` z ) C_ ( rank ` w ) ) )
29 27 28 bitr4di 
 |-  ( x = z -> ( A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) )
30 14 29 anbi12d 
 |-  ( x = z -> ( ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) ) )
31 10 11 30 elabf 
 |-  ( z e. { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) } <-> ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) )
32 31 bicomi 
 |-  ( ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) <-> z e. { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) } )
33 5 32 mpgbir 
 |-  { z | ( z e. { x | ph } /\ A. w e. { x | ph } ( rank ` z ) C_ ( rank ` w ) ) } = { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) }
34 3 4 33 3eqtri 
 |-  Scott { x | ph } = { x | ( ph /\ A. y ( ps -> ( rank ` x ) C_ ( rank ` y ) ) ) }