Metamath Proof Explorer

Theorem dfno2

Description: A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025)

Ref Expression
Assertion dfno2 
|- No = { f e. ~P ( On X. { 1o , 2o } ) | ( Fun f /\ dom f e. On ) }

Proof

Step Hyp Ref Expression
1 fssxp 
 |-  ( f : x --> { 1o , 2o } -> f C_ ( x X. { 1o , 2o } ) )
2 1 adantl 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> f C_ ( x X. { 1o , 2o } ) )
3 onss 
 |-  ( x e. On -> x C_ On )
4 3 adantr 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> x C_ On )
5 xpss1 
 |-  ( x C_ On -> ( x X. { 1o , 2o } ) C_ ( On X. { 1o , 2o } ) )
6 4 5 syl 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> ( x X. { 1o , 2o } ) C_ ( On X. { 1o , 2o } ) )
7 2 6 sstrd 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> f C_ ( On X. { 1o , 2o } ) )
8 velpw 
 |-  ( f e. ~P ( On X. { 1o , 2o } ) <-> f C_ ( On X. { 1o , 2o } ) )
9 7 8 sylibr 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> f e. ~P ( On X. { 1o , 2o } ) )
10 ffun 
 |-  ( f : x --> { 1o , 2o } -> Fun f )
11 10 adantl 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> Fun f )
12 fdm 
 |-  ( f : x --> { 1o , 2o } -> dom f = x )
13 12 adantl 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> dom f = x )
14 simpl 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> x e. On )
15 13 14 eqeltrd 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> dom f e. On )
16 9 11 15 jca32 
 |-  ( ( x e. On /\ f : x --> { 1o , 2o } ) -> ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) )
17 16 rexlimiva 
 |-  ( E. x e. On f : x --> { 1o , 2o } -> ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) )
18 simprr 
 |-  ( ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) -> dom f e. On )
19 feq2 
 |-  ( x = dom f -> ( f : x --> { 1o , 2o } <-> f : dom f --> { 1o , 2o } ) )
20 19 adantl 
 |-  ( ( ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) /\ x = dom f ) -> ( f : x --> { 1o , 2o } <-> f : dom f --> { 1o , 2o } ) )
21 simpl 
 |-  ( ( Fun f /\ dom f e. On ) -> Fun f )
22 elpwi 
 |-  ( f e. ~P ( On X. { 1o , 2o } ) -> f C_ ( On X. { 1o , 2o } ) )
23 funssxp 
 |-  ( ( Fun f /\ f C_ ( On X. { 1o , 2o } ) ) <-> ( f : dom f --> { 1o , 2o } /\ dom f C_ On ) )
24 23 simplbi 
 |-  ( ( Fun f /\ f C_ ( On X. { 1o , 2o } ) ) -> f : dom f --> { 1o , 2o } )
25 21 22 24 syl2anr 
 |-  ( ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) -> f : dom f --> { 1o , 2o } )
26 18 20 25 rspcedvd 
 |-  ( ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) -> E. x e. On f : x --> { 1o , 2o } )
27 17 26 impbii 
 |-  ( E. x e. On f : x --> { 1o , 2o } <-> ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) )
28 27 abbii 
 |-  { f | E. x e. On f : x --> { 1o , 2o } } = { f | ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) }
29 df-no 
 |-  No = { f | E. x e. On f : x --> { 1o , 2o } }
30 df-rab 
 |-  { f e. ~P ( On X. { 1o , 2o } ) | ( Fun f /\ dom f e. On ) } = { f | ( f e. ~P ( On X. { 1o , 2o } ) /\ ( Fun f /\ dom f e. On ) ) }
31 28 29 30 3eqtr4i 
 |-  No = { f e. ~P ( On X. { 1o , 2o } ) | ( Fun f /\ dom f e. On ) }