Metamath Proof Explorer

Theorem nosupcbv

Description: Lemma to change bound variables in a surreal supremum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis nosupcbv.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 nosupcbv 
|- S = if ( E. a e. A A. b e. A -. a . } ) , ( c e. { d | E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) } |-> ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) ) )

Proof

Step Hyp Ref Expression
1 nosupcbv.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 breq1 
 |-  ( x = a -> ( x  a
3 2 notbid 
 |-  ( x = a -> ( -. x  -. a
4 3 ralbidv 
 |-  ( x = a -> ( A. y e. A -. x  A. y e. A -. a
5 breq2 
 |-  ( y = b -> ( a  a
6 5 notbid 
 |-  ( y = b -> ( -. a  -. a
7 6 cbvralvw 
 |-  ( A. y e. A -. a  A. b e. A -. a
8 4 7 bitrdi 
 |-  ( x = a -> ( A. y e. A -. x  A. b e. A -. a
9 8 cbvrexvw 
 |-  ( E. x e. A A. y e. A -. x  E. a e. A A. b e. A -. a
10 8 cbvriotavw 
 |-  ( iota_ x e. A A. y e. A -. x
11 10 dmeqi 
 |-  dom ( iota_ x e. A A. y e. A -. x
12 11 opeq1i 
 |-  <. dom ( iota_ x e. A A. y e. A -. x . = <. dom ( iota_ a e. A A. b e. A -. a .
13 12 sneqi 
 |-  { <. dom ( iota_ x e. A A. y e. A -. x . } = { <. dom ( iota_ a e. A A. b e. A -. a . }
14 10 13 uneq12i 
 |-  ( ( iota_ x e. A A. y e. A -. x . } ) = ( ( iota_ a e. A A. b e. A -. a . } )
15 eleq1w 
 |-  ( g = c -> ( g e. dom u <-> c e. dom u ) )
16 suceq 
 |-  ( g = c -> suc g = suc c )
17 16 reseq2d 
 |-  ( g = c -> ( u |` suc g ) = ( u |` suc c ) )
18 16 reseq2d 
 |-  ( g = c -> ( v |` suc g ) = ( v |` suc c ) )
19 17 18 eqeq12d 
 |-  ( g = c -> ( ( u |` suc g ) = ( v |` suc g ) <-> ( u |` suc c ) = ( v |` suc c ) ) )
20 19 imbi2d 
 |-  ( g = c -> ( ( -. v  ( u |` suc g ) = ( v |` suc g ) ) <-> ( -. v  ( u |` suc c ) = ( v |` suc c ) ) ) )
21 20 ralbidv 
 |-  ( g = c -> ( A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) <-> A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) ) )
22 fveqeq2 
 |-  ( g = c -> ( ( u ` g ) = x <-> ( u ` c ) = x ) )
23 15 21 22 3anbi123d 
 |-  ( g = c -> ( ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) <-> ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = x ) ) )
24 23 rexbidv 
 |-  ( g = c -> ( E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) <-> E. u e. A ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = x ) ) )
25 24 iotabidv 
 |-  ( g = c -> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = ( iota x E. u e. A ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = x ) ) )
26 eqeq2 
 |-  ( x = a -> ( ( u ` c ) = x <-> ( u ` c ) = a ) )
27 26 3anbi3d 
 |-  ( x = a -> ( ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = x ) <-> ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = a ) ) )
28 27 rexbidv 
 |-  ( x = a -> ( E. u e. A ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = x ) <-> E. u e. A ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = a ) ) )
29 dmeq 
 |-  ( u = e -> dom u = dom e )
30 29 eleq2d 
 |-  ( u = e -> ( c e. dom u <-> c e. dom e ) )
31 breq2 
 |-  ( u = e -> ( v  v
32 31 notbid 
 |-  ( u = e -> ( -. v  -. v
33 reseq1 
 |-  ( u = e -> ( u |` suc c ) = ( e |` suc c ) )
34 33 eqeq1d 
 |-  ( u = e -> ( ( u |` suc c ) = ( v |` suc c ) <-> ( e |` suc c ) = ( v |` suc c ) ) )
35 32 34 imbi12d 
 |-  ( u = e -> ( ( -. v  ( u |` suc c ) = ( v |` suc c ) ) <-> ( -. v  ( e |` suc c ) = ( v |` suc c ) ) ) )
36 35 ralbidv 
 |-  ( u = e -> ( A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) <-> A. v e. A ( -. v  ( e |` suc c ) = ( v |` suc c ) ) ) )
37 breq1 
 |-  ( v = f -> ( v  f
38 37 notbid 
 |-  ( v = f -> ( -. v  -. f
39 reseq1 
 |-  ( v = f -> ( v |` suc c ) = ( f |` suc c ) )
40 39 eqeq2d 
 |-  ( v = f -> ( ( e |` suc c ) = ( v |` suc c ) <-> ( e |` suc c ) = ( f |` suc c ) ) )
41 38 40 imbi12d 
 |-  ( v = f -> ( ( -. v  ( e |` suc c ) = ( v |` suc c ) ) <-> ( -. f  ( e |` suc c ) = ( f |` suc c ) ) ) )
42 41 cbvralvw 
 |-  ( A. v e. A ( -. v  ( e |` suc c ) = ( v |` suc c ) ) <-> A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) )
43 36 42 bitrdi 
 |-  ( u = e -> ( A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) <-> A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) ) )
44 fveq1 
 |-  ( u = e -> ( u ` c ) = ( e ` c ) )
45 44 eqeq1d 
 |-  ( u = e -> ( ( u ` c ) = a <-> ( e ` c ) = a ) )
46 30 43 45 3anbi123d 
 |-  ( u = e -> ( ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = a ) <-> ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) )
47 46 cbvrexvw 
 |-  ( E. u e. A ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = a ) <-> E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) )
48 28 47 bitrdi 
 |-  ( x = a -> ( E. u e. A ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = x ) <-> E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) )
49 48 cbviotavw 
 |-  ( iota x E. u e. A ( c e. dom u /\ A. v e. A ( -. v  ( u |` suc c ) = ( v |` suc c ) ) /\ ( u ` c ) = x ) ) = ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) )
50 25 49 eqtrdi 
 |-  ( g = c -> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) = ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) )
51 50 cbvmptv 
 |-  ( 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 ) ) ) = ( c e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) )
52 eleq1w 
 |-  ( y = d -> ( y e. dom u <-> d e. dom u ) )
53 suceq 
 |-  ( y = d -> suc y = suc d )
54 53 reseq2d 
 |-  ( y = d -> ( u |` suc y ) = ( u |` suc d ) )
55 53 reseq2d 
 |-  ( y = d -> ( v |` suc y ) = ( v |` suc d ) )
56 54 55 eqeq12d 
 |-  ( y = d -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc d ) = ( v |` suc d ) ) )
57 56 imbi2d 
 |-  ( y = d -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. v  ( u |` suc d ) = ( v |` suc d ) ) ) )
58 57 ralbidv 
 |-  ( y = d -> ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. v e. A ( -. v  ( u |` suc d ) = ( v |` suc d ) ) ) )
59 52 58 anbi12d 
 |-  ( y = d -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( d e. dom u /\ A. v e. A ( -. v  ( u |` suc d ) = ( v |` suc d ) ) ) ) )
60 59 rexbidv 
 |-  ( y = d -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. u e. A ( d e. dom u /\ A. v e. A ( -. v  ( u |` suc d ) = ( v |` suc d ) ) ) ) )
61 29 eleq2d 
 |-  ( u = e -> ( d e. dom u <-> d e. dom e ) )
62 reseq1 
 |-  ( u = e -> ( u |` suc d ) = ( e |` suc d ) )
63 62 eqeq1d 
 |-  ( u = e -> ( ( u |` suc d ) = ( v |` suc d ) <-> ( e |` suc d ) = ( v |` suc d ) ) )
64 32 63 imbi12d 
 |-  ( u = e -> ( ( -. v  ( u |` suc d ) = ( v |` suc d ) ) <-> ( -. v  ( e |` suc d ) = ( v |` suc d ) ) ) )
65 64 ralbidv 
 |-  ( u = e -> ( A. v e. A ( -. v  ( u |` suc d ) = ( v |` suc d ) ) <-> A. v e. A ( -. v  ( e |` suc d ) = ( v |` suc d ) ) ) )
66 reseq1 
 |-  ( v = f -> ( v |` suc d ) = ( f |` suc d ) )
67 66 eqeq2d 
 |-  ( v = f -> ( ( e |` suc d ) = ( v |` suc d ) <-> ( e |` suc d ) = ( f |` suc d ) ) )
68 38 67 imbi12d 
 |-  ( v = f -> ( ( -. v  ( e |` suc d ) = ( v |` suc d ) ) <-> ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) )
69 68 cbvralvw 
 |-  ( A. v e. A ( -. v  ( e |` suc d ) = ( v |` suc d ) ) <-> A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) )
70 65 69 bitrdi 
 |-  ( u = e -> ( A. v e. A ( -. v  ( u |` suc d ) = ( v |` suc d ) ) <-> A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) )
71 61 70 anbi12d 
 |-  ( u = e -> ( ( d e. dom u /\ A. v e. A ( -. v  ( u |` suc d ) = ( v |` suc d ) ) ) <-> ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) ) )
72 71 cbvrexvw 
 |-  ( E. u e. A ( d e. dom u /\ A. v e. A ( -. v  ( u |` suc d ) = ( v |` suc d ) ) ) <-> E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) )
73 60 72 bitrdi 
 |-  ( y = d -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) ) )
74 73 cbvabv 
 |-  { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } = { d | E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) }
75 74 mpteq1i 
 |-  ( c e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) ) = ( c e. { d | E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) } |-> ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) )
76 51 75 eqtri 
 |-  ( 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 ) ) ) = ( c e. { d | E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) } |-> ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) )
77 9 14 76 ifbieq12i 
 |-  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 ) ) ) ) = if ( E. a e. A A. b e. A -. a . } ) , ( c e. { d | E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) } |-> ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) ) )
78 1 77 eqtri 
 |-  S = if ( E. a e. A A. b e. A -. a . } ) , ( c e. { d | E. e e. A ( d e. dom e /\ A. f e. A ( -. f  ( e |` suc d ) = ( f |` suc d ) ) ) } |-> ( iota a E. e e. A ( c e. dom e /\ A. f e. A ( -. f  ( e |` suc c ) = ( f |` suc c ) ) /\ ( e ` c ) = a ) ) ) )