Metamath Proof Explorer

Theorem noinfdm

Description: Next, we calculate the domain of T . This is mostly to change bound variables. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Hypothesis noinfdm.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 noinfdm 
|- ( -. E. x e. B A. y e. B -. y  dom T = { z | E. p e. B ( z e. dom p /\ A. q e. B ( -. p  ( p |` suc z ) = ( q |` suc z ) ) ) } )

Proof

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