Metamath Proof Explorer

Theorem dfscott3

Description: Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026)

Ref Expression
Assertion dfscott3 
|- Scott A = ( A i^i ( R1 ` suc |^| ( rank " A ) ) )

Proof

Step Hyp Ref Expression
1 dfscott2 
 |-  Scott A = { x e. A | ( rank ` x ) = |^| ( rank " A ) }
2 rankfn 
 |-  rank Fn _V
3 ssv 
 |-  A C_ _V
4 fnfvima 
 |-  ( ( rank Fn _V /\ A C_ _V /\ x e. A ) -> ( rank ` x ) e. ( rank " A ) )
5 2 3 4 mp3an12 
 |-  ( x e. A -> ( rank ` x ) e. ( rank " A ) )
6 intss1 
 |-  ( ( rank ` x ) e. ( rank " A ) -> |^| ( rank " A ) C_ ( rank ` x ) )
7 5 6 syl 
 |-  ( x e. A -> |^| ( rank " A ) C_ ( rank ` x ) )
8 ne0i 
 |-  ( x e. A -> A =/= (/) )
9 rankfo 
 |-  rank : _V -onto-> On
10 fof 
 |-  ( rank : _V -onto-> On -> rank : _V --> On )
11 9 10 ax-mp 
 |-  rank : _V --> On
12 11 fdmi 
 |-  dom rank = _V
13 12 ineq1i 
 |-  ( dom rank i^i A ) = ( _V i^i A )
14 inv2 
 |-  ( _V i^i A ) = A
15 13 14 eqtri 
 |-  ( dom rank i^i A ) = A
16 15 neeq1i 
 |-  ( ( dom rank i^i A ) =/= (/) <-> A =/= (/) )
17 16 biimpri 
 |-  ( A =/= (/) -> ( dom rank i^i A ) =/= (/) )
18 17 imadisjlnd 
 |-  ( A =/= (/) -> ( rank " A ) =/= (/) )
19 fimass 
 |-  ( rank : _V --> On -> ( rank " A ) C_ On )
20 11 19 ax-mp 
 |-  ( rank " A ) C_ On
21 oninton 
 |-  ( ( ( rank " A ) C_ On /\ ( rank " A ) =/= (/) ) -> |^| ( rank " A ) e. On )
22 20 21 mpan 
 |-  ( ( rank " A ) =/= (/) -> |^| ( rank " A ) e. On )
23 vex 
 |-  x e. _V
24 23 ssrankr1 
 |-  ( |^| ( rank " A ) e. On -> ( |^| ( rank " A ) C_ ( rank ` x ) <-> -. x e. ( R1 ` |^| ( rank " A ) ) ) )
25 8 18 22 24 4syl 
 |-  ( x e. A -> ( |^| ( rank " A ) C_ ( rank ` x ) <-> -. x e. ( R1 ` |^| ( rank " A ) ) ) )
26 7 25 mpbid 
 |-  ( x e. A -> -. x e. ( R1 ` |^| ( rank " A ) ) )
27 26 biantrurd 
 |-  ( x e. A -> ( x e. ( R1 ` suc |^| ( rank " A ) ) <-> ( -. x e. ( R1 ` |^| ( rank " A ) ) /\ x e. ( R1 ` suc |^| ( rank " A ) ) ) ) )
28 23 rankr1 
 |-  ( |^| ( rank " A ) = ( rank ` x ) <-> ( -. x e. ( R1 ` |^| ( rank " A ) ) /\ x e. ( R1 ` suc |^| ( rank " A ) ) ) )
29 27 28 bitr4di 
 |-  ( x e. A -> ( x e. ( R1 ` suc |^| ( rank " A ) ) <-> |^| ( rank " A ) = ( rank ` x ) ) )
30 eqcom 
 |-  ( ( rank ` x ) = |^| ( rank " A ) <-> |^| ( rank " A ) = ( rank ` x ) )
31 29 30 bitr4di 
 |-  ( x e. A -> ( x e. ( R1 ` suc |^| ( rank " A ) ) <-> ( rank ` x ) = |^| ( rank " A ) ) )
32 31 adantl 
 |-  ( ( T. /\ x e. A ) -> ( x e. ( R1 ` suc |^| ( rank " A ) ) <-> ( rank ` x ) = |^| ( rank " A ) ) )
33 32 rabbi2dva 
 |-  ( T. -> ( A i^i ( R1 ` suc |^| ( rank " A ) ) ) = { x e. A | ( rank ` x ) = |^| ( rank " A ) } )
34 33 mptru 
 |-  ( A i^i ( R1 ` suc |^| ( rank " A ) ) ) = { x e. A | ( rank ` x ) = |^| ( rank " A ) }
35 1 34 eqtr4i 
 |-  Scott A = ( A i^i ( R1 ` suc |^| ( rank " A ) ) )