Metamath Proof Explorer

Theorem nosupdm

Description: The domain of the surreal supremum when there is no maximum. The primary point of this theorem is to change bound variable. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Hypothesis nosupdm.1 
|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion nosupdm 
|- ( -. E. x e. A A. y e. A -. x  dom S = { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) } )

Proof

Step Hyp Ref Expression
1 nosupdm.1 
 |-  S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2 iffalse 
 |-  ( -. E. x e. A A. y e. A -. x  if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ) = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
3 1 2 syl5eq 
 |-  ( -. E. x e. A A. y e. A -. x  S = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
4 3 dmeqd 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = dom ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
5 iotaex 
 |-  ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) e. _V
6 eqid 
 |-  ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) )
7 5 6 dmmpti 
 |-  dom ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) }
8 4 7 eqtrdi 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
9 dmeq 
 |-  ( u = p -> dom u = dom p )
10 9 eleq2d 
 |-  ( u = p -> ( y e. dom u <-> y e. dom p ) )
11 breq1 
 |-  ( v = q -> ( v  q
12 11 notbid 
 |-  ( v = q -> ( -. v  -. q
13 reseq1 
 |-  ( v = q -> ( v |` suc y ) = ( q |` suc y ) )
14 13 eqeq2d 
 |-  ( v = q -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc y ) = ( q |` suc y ) ) )
15 12 14 imbi12d 
 |-  ( v = q -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. q  ( u |` suc y ) = ( q |` suc y ) ) ) )
16 15 cbvralvw 
 |-  ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. q e. A ( -. q  ( u |` suc y ) = ( q |` suc y ) ) )
17 breq2 
 |-  ( u = p -> ( q  q
18 17 notbid 
 |-  ( u = p -> ( -. q  -. q
19 reseq1 
 |-  ( u = p -> ( u |` suc y ) = ( p |` suc y ) )
20 19 eqeq1d 
 |-  ( u = p -> ( ( u |` suc y ) = ( q |` suc y ) <-> ( p |` suc y ) = ( q |` suc y ) ) )
21 18 20 imbi12d 
 |-  ( u = p -> ( ( -. q  ( u |` suc y ) = ( q |` suc y ) ) <-> ( -. q  ( p |` suc y ) = ( q |` suc y ) ) ) )
22 21 ralbidv 
 |-  ( u = p -> ( A. q e. A ( -. q  ( u |` suc y ) = ( q |` suc y ) ) <-> A. q e. A ( -. q  ( p |` suc y ) = ( q |` suc y ) ) ) )
23 16 22 syl5bb 
 |-  ( u = p -> ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. q e. A ( -. q  ( p |` suc y ) = ( q |` suc y ) ) ) )
24 10 23 anbi12d 
 |-  ( u = p -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( y e. dom p /\ A. q e. A ( -. q  ( p |` suc y ) = ( q |` suc y ) ) ) ) )
25 24 cbvrexvw 
 |-  ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. p e. A ( y e. dom p /\ A. q e. A ( -. q  ( p |` suc y ) = ( q |` suc y ) ) ) )
26 eleq1w 
 |-  ( y = z -> ( y e. dom p <-> z e. dom p ) )
27 suceq 
 |-  ( y = z -> suc y = suc z )
28 27 reseq2d 
 |-  ( y = z -> ( p |` suc y ) = ( p |` suc z ) )
29 27 reseq2d 
 |-  ( y = z -> ( q |` suc y ) = ( q |` suc z ) )
30 28 29 eqeq12d 
 |-  ( y = z -> ( ( p |` suc y ) = ( q |` suc y ) <-> ( p |` suc z ) = ( q |` suc z ) ) )
31 30 imbi2d 
 |-  ( y = z -> ( ( -. q  ( p |` suc y ) = ( q |` suc y ) ) <-> ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) )
32 31 ralbidv 
 |-  ( y = z -> ( A. q e. A ( -. q  ( p |` suc y ) = ( q |` suc y ) ) <-> A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) )
33 26 32 anbi12d 
 |-  ( y = z -> ( ( y e. dom p /\ A. q e. A ( -. q  ( p |` suc y ) = ( q |` suc y ) ) ) <-> ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) ) )
34 33 rexbidv 
 |-  ( y = z -> ( E. p e. A ( y e. dom p /\ A. q e. A ( -. q  ( p |` suc y ) = ( q |` suc y ) ) ) <-> E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) ) )
35 25 34 syl5bb 
 |-  ( y = z -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) ) )
36 35 cbvabv 
 |-  { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } = { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) }
37 8 36 eqtrdi 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = { z | E. p e. A ( z e. dom p /\ A. q e. A ( -. q  ( p |` suc z ) = ( q |` suc z ) ) ) } )