Metamath Proof Explorer

Theorem noinfcbv

Description: Change bound variables for surreal infimum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfcbv.1 
|- T = if ( E. x e. B A. y e. B -. y . } ) , ( g e. { y | E. u e. B ( y e. dom u /\ A. v e. B ( -. u  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. B ( g e. dom u /\ A. v e. B ( -. u  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion noinfcbv 
|- T = if ( E. a e. B A. b e. B -. b . } ) , ( c e. { b | E. d e. B ( b e. dom d /\ A. e e. B ( -. d  ( d |` suc b ) = ( e |` suc b ) ) ) } |-> ( iota a E. d e. B ( c e. dom d /\ A. e e. B ( -. d  ( d |` suc c ) = ( e |` suc c ) ) /\ ( d ` c ) = a ) ) ) )

Proof

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