Metamath Proof Explorer

Theorem noetasuplem2

Description: Lemma for noeta . The restriction of Z to dom S is S . (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

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