Metamath Proof Explorer

Theorem noetainflem2

Description: Lemma for noeta . The restriction of W to the domain of T is T . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetainflem.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 ) ) ) )
noetainflem.2 
|- W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
Assertion noetainflem2 
|- ( ( B C_ No /\ B e. _V ) -> ( W |` dom T ) = T )

Proof

Step Hyp Ref Expression
1 noetainflem.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 noetainflem.2 
 |-  W = ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
3 2 reseq1i 
 |-  ( W |` dom T ) = ( ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) |` dom T )
4 resundir 
 |-  ( ( T u. ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) |` dom T ) = ( ( T |` dom T ) u. ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) )
5 3 4 eqtri 
 |-  ( W |` dom T ) = ( ( T |` dom T ) u. ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) )
6 1 noinfno 
 |-  ( ( B C_ No /\ B e. _V ) -> T e. No )
7 nofun 
 |-  ( T e. No -> Fun T )
8 funrel 
 |-  ( Fun T -> Rel T )
9 resdm 
 |-  ( Rel T -> ( T |` dom T ) = T )
10 6 7 8 9 4syl 
 |-  ( ( B C_ No /\ B e. _V ) -> ( T |` dom T ) = T )
11 dmres 
 |-  dom ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = ( dom T i^i dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) )
12 2oex 
 |-  2o e. _V
13 12 snnz 
 |-  { 2o } =/= (/)
14 dmxp 
 |-  ( { 2o } =/= (/) -> dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) = ( suc U. ( bday " A ) \ dom T ) )
15 13 14 ax-mp 
 |-  dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) = ( suc U. ( bday " A ) \ dom T )
16 15 ineq2i 
 |-  ( dom T i^i dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) = ( dom T i^i ( suc U. ( bday " A ) \ dom T ) )
17 disjdif 
 |-  ( dom T i^i ( suc U. ( bday " A ) \ dom T ) ) = (/)
18 16 17 eqtri 
 |-  ( dom T i^i dom ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) ) = (/)
19 11 18 eqtri 
 |-  dom ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = (/)
20 relres 
 |-  Rel ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T )
21 reldm0 
 |-  ( Rel ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) -> ( ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = (/) <-> dom ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = (/) ) )
22 20 21 ax-mp 
 |-  ( ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = (/) <-> dom ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = (/) )
23 19 22 mpbir 
 |-  ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = (/)
24 23 a1i 
 |-  ( ( B C_ No /\ B e. _V ) -> ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) = (/) )
25 10 24 uneq12d 
 |-  ( ( B C_ No /\ B e. _V ) -> ( ( T |` dom T ) u. ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) ) = ( T u. (/) ) )
26 un0 
 |-  ( T u. (/) ) = T
27 25 26 eqtrdi 
 |-  ( ( B C_ No /\ B e. _V ) -> ( ( T |` dom T ) u. ( ( ( suc U. ( bday " A ) \ dom T ) X. { 2o } ) |` dom T ) ) = T )
28 5 27 eqtrid 
 |-  ( ( B C_ No /\ B e. _V ) -> ( W |` dom T ) = T )