Metamath Proof Explorer

Theorem nosupres

Description: A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupres.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 nosupres 
|- ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( S |` suc G ) = ( U |` suc G ) )

Proof

Step Hyp Ref Expression
1 nosupres.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 dmres 
 |-  dom ( S |` suc G ) = ( suc G i^i dom S )
3 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
4 3 3ad2ant2 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> S e. No )
5 nodmord 
 |-  ( S e. No -> Ord dom S )
6 4 5 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Ord dom S )
7 dmeq 
 |-  ( p = U -> dom p = dom U )
8 7 eleq2d 
 |-  ( p = U -> ( G e. dom p <-> G e. dom U ) )
9 breq2 
 |-  ( p = U -> ( v  v
10 9 notbid 
 |-  ( p = U -> ( -. v  -. v
11 reseq1 
 |-  ( p = U -> ( p |` suc G ) = ( U |` suc G ) )
12 11 eqeq1d 
 |-  ( p = U -> ( ( p |` suc G ) = ( v |` suc G ) <-> ( U |` suc G ) = ( v |` suc G ) ) )
13 10 12 imbi12d 
 |-  ( p = U -> ( ( -. v  ( p |` suc G ) = ( v |` suc G ) ) <-> ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) )
14 13 ralbidv 
 |-  ( p = U -> ( A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) <-> A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) )
15 8 14 anbi12d 
 |-  ( p = U -> ( ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) <-> ( G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) ) )
16 15 rspcev 
 |-  ( ( U e. A /\ ( G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> E. p e. A ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
17 16 3impb 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. p e. A ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
18 dmeq 
 |-  ( u = p -> dom u = dom p )
19 18 eleq2d 
 |-  ( u = p -> ( G e. dom u <-> G e. dom p ) )
20 breq2 
 |-  ( u = p -> ( v  v
21 20 notbid 
 |-  ( u = p -> ( -. v  -. v
22 reseq1 
 |-  ( u = p -> ( u |` suc G ) = ( p |` suc G ) )
23 22 eqeq1d 
 |-  ( u = p -> ( ( u |` suc G ) = ( v |` suc G ) <-> ( p |` suc G ) = ( v |` suc G ) ) )
24 21 23 imbi12d 
 |-  ( u = p -> ( ( -. v  ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
25 24 ralbidv 
 |-  ( u = p -> ( A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) <-> A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
26 19 25 anbi12d 
 |-  ( u = p -> ( ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) <-> ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) ) )
27 26 cbvrexvw 
 |-  ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) <-> E. p e. A ( G e. dom p /\ A. v e. A ( -. v  ( p |` suc G ) = ( v |` suc G ) ) ) )
28 17 27 sylibr 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
29 eleq1 
 |-  ( y = G -> ( y e. dom u <-> G e. dom u ) )
30 suceq 
 |-  ( y = G -> suc y = suc G )
31 30 reseq2d 
 |-  ( y = G -> ( u |` suc y ) = ( u |` suc G ) )
32 30 reseq2d 
 |-  ( y = G -> ( v |` suc y ) = ( v |` suc G ) )
33 31 32 eqeq12d 
 |-  ( y = G -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc G ) = ( v |` suc G ) ) )
34 33 imbi2d 
 |-  ( y = G -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
35 34 ralbidv 
 |-  ( y = G -> ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) )
36 29 35 anbi12d 
 |-  ( y = G -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
37 36 rexbidv 
 |-  ( y = G -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
38 37 elabg 
 |-  ( G e. dom U -> ( G e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
39 38 3ad2ant2 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> ( G e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. v  ( u |` suc G ) = ( v |` suc G ) ) ) ) )
40 28 39 mpbird 
 |-  ( ( U e. A /\ G e. dom U /\ A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) ) -> G e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
41 40 3ad2ant3 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
42 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 ) ) ) )
43 1 42 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 ) ) ) )
44 43 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 ) ) ) )
45 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
46 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 ) ) )
47 45 46 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 ) ) ) }
48 44 47 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 ) ) ) } )
49 48 3ad2ant1 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom S = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
50 41 49 eleqtrrd 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. dom S )
51 ordsucss 
 |-  ( Ord dom S -> ( G e. dom S -> suc G C_ dom S ) )
52 6 50 51 sylc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> suc G C_ dom S )
53 df-ss 
 |-  ( suc G C_ dom S <-> ( suc G i^i dom S ) = suc G )
54 52 53 sylib 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( suc G i^i dom S ) = suc G )
55 2 54 syl5eq 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom ( S |` suc G ) = suc G )
56 dmres 
 |-  dom ( U |` suc G ) = ( suc G i^i dom U )
57 simp2l 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> A C_ No )
58 simp31 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> U e. A )
59 57 58 sseldd 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> U e. No )
60 nodmord 
 |-  ( U e. No -> Ord dom U )
61 59 60 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Ord dom U )
62 simp32 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. dom U )
63 ordsucss 
 |-  ( Ord dom U -> ( G e. dom U -> suc G C_ dom U ) )
64 61 62 63 sylc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> suc G C_ dom U )
65 df-ss 
 |-  ( suc G C_ dom U <-> ( suc G i^i dom U ) = suc G )
66 64 65 sylib 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( suc G i^i dom U ) = suc G )
67 56 66 syl5eq 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom ( U |` suc G ) = suc G )
68 55 67 eqtr4d 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom ( S |` suc G ) = dom ( U |` suc G ) )
69 55 eleq2d 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( a e. dom ( S |` suc G ) <-> a e. suc G ) )
70 simpl1 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> -. E. x e. A A. y e. A -. x
71 simpl2 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( A C_ No /\ A e. _V ) )
72 simpl31 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> U e. A )
73 64 sselda 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> a e. dom U )
74 nodmon 
 |-  ( U e. No -> dom U e. On )
75 59 74 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> dom U e. On )
76 onelon 
 |-  ( ( dom U e. On /\ G e. dom U ) -> G e. On )
77 75 62 76 syl2anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> G e. On )
78 eloni 
 |-  ( G e. On -> Ord G )
79 77 78 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Ord G )
80 ordsuc 
 |-  ( Ord G <-> Ord suc G )
81 79 80 sylib 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Ord suc G )
82 ordsucss 
 |-  ( Ord suc G -> ( a e. suc G -> suc a C_ suc G ) )
83 81 82 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( a e. suc G -> suc a C_ suc G ) )
84 83 imp 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> suc a C_ suc G )
85 simpl33 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) )
86 reseq1 
 |-  ( ( U |` suc G ) = ( v |` suc G ) -> ( ( U |` suc G ) |` suc a ) = ( ( v |` suc G ) |` suc a ) )
87 resabs1 
 |-  ( suc a C_ suc G -> ( ( U |` suc G ) |` suc a ) = ( U |` suc a ) )
88 resabs1 
 |-  ( suc a C_ suc G -> ( ( v |` suc G ) |` suc a ) = ( v |` suc a ) )
89 87 88 eqeq12d 
 |-  ( suc a C_ suc G -> ( ( ( U |` suc G ) |` suc a ) = ( ( v |` suc G ) |` suc a ) <-> ( U |` suc a ) = ( v |` suc a ) ) )
90 86 89 syl5ib 
 |-  ( suc a C_ suc G -> ( ( U |` suc G ) = ( v |` suc G ) -> ( U |` suc a ) = ( v |` suc a ) ) )
91 90 imim2d 
 |-  ( suc a C_ suc G -> ( ( -. v  ( U |` suc G ) = ( v |` suc G ) ) -> ( -. v  ( U |` suc a ) = ( v |` suc a ) ) ) )
92 91 ralimdv 
 |-  ( suc a C_ suc G -> ( A. v e. A ( -. v  ( U |` suc G ) = ( v |` suc G ) ) -> A. v e. A ( -. v  ( U |` suc a ) = ( v |` suc a ) ) ) )
93 84 85 92 sylc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> A. v e. A ( -. v  ( U |` suc a ) = ( v |` suc a ) ) )
94 1 nosupfv 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc a ) = ( v |` suc a ) ) ) ) -> ( S ` a ) = ( U ` a ) )
95 70 71 72 73 93 94 syl113anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( S ` a ) = ( U ` a ) )
96 simpr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> a e. suc G )
97 96 fvresd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( ( S |` suc G ) ` a ) = ( S ` a ) )
98 96 fvresd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( ( U |` suc G ) ` a ) = ( U ` a ) )
99 95 97 98 3eqtr4d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) /\ a e. suc G ) -> ( ( S |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) )
100 99 ex 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( a e. suc G -> ( ( S |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) )
101 69 100 sylbid 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( a e. dom ( S |` suc G ) -> ( ( S |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) )
102 101 ralrimiv 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> A. a e. dom ( S |` suc G ) ( ( S |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) )
103 nofun 
 |-  ( S e. No -> Fun S )
104 funres 
 |-  ( Fun S -> Fun ( S |` suc G ) )
105 4 103 104 3syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Fun ( S |` suc G ) )
106 nofun 
 |-  ( U e. No -> Fun U )
107 funres 
 |-  ( Fun U -> Fun ( U |` suc G ) )
108 59 106 107 3syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> Fun ( U |` suc G ) )
109 eqfunfv 
 |-  ( ( Fun ( S |` suc G ) /\ Fun ( U |` suc G ) ) -> ( ( S |` suc G ) = ( U |` suc G ) <-> ( dom ( S |` suc G ) = dom ( U |` suc G ) /\ A. a e. dom ( S |` suc G ) ( ( S |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) ) )
110 105 108 109 syl2anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( ( S |` suc G ) = ( U |` suc G ) <-> ( dom ( S |` suc G ) = dom ( U |` suc G ) /\ A. a e. dom ( S |` suc G ) ( ( S |` suc G ) ` a ) = ( ( U |` suc G ) ` a ) ) ) )
111 68 102 110 mpbir2and 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` suc G ) = ( v |` suc G ) ) ) ) -> ( S |` suc G ) = ( U |` suc G ) )