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