Metamath Proof Explorer

Theorem noetasuplem3

Description: Lemma for noeta . Z is an upper bound for A . Part of Theorem 5.1 of Lipparini p. 7-8. (Contributed by Scott Fenton, 4-Dec-2021)

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 noetasuplem3 
|- ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> X

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 simpl1 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> A C_ No )
4 simpl2 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> A e. _V )
5 simpr 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> X e. A )
6 1 nosupbnd1 
 |-  ( ( A C_ No /\ A e. _V /\ X e. A ) -> ( X |` dom S )
7 3 4 5 6 syl3anc 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> ( X |` dom S )
8 2 reseq1i 
 |-  ( Z |` dom S ) = ( ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) |` dom S )
9 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 ) )
10 df-res 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) |` dom S ) = ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) i^i ( dom S X. _V ) )
11 incom 
 |-  ( ( suc U. ( bday " B ) \ dom S ) i^i dom S ) = ( dom S i^i ( suc U. ( bday " B ) \ dom S ) )
12 disjdif 
 |-  ( dom S i^i ( suc U. ( bday " B ) \ dom S ) ) = (/)
13 11 12 eqtri 
 |-  ( ( suc U. ( bday " B ) \ dom S ) i^i dom S ) = (/)
14 xpdisj1 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) i^i dom S ) = (/) -> ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) i^i ( dom S X. _V ) ) = (/) )
15 13 14 ax-mp 
 |-  ( ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) i^i ( dom S X. _V ) ) = (/)
16 10 15 eqtri 
 |-  ( ( ( 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 un0 
 |-  ( ( S |` dom S ) u. (/) ) = ( S |` dom S )
19 9 17 18 3eqtri 
 |-  ( ( S u. ( ( suc U. ( bday " B ) \ dom S ) X. { 1o } ) ) |` dom S ) = ( S |` dom S )
20 8 19 eqtri 
 |-  ( Z |` dom S ) = ( S |` dom S )
21 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
22 3 4 21 syl2anc 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> S e. No )
23 nofun 
 |-  ( S e. No -> Fun S )
24 22 23 syl 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> Fun S )
25 funrel 
 |-  ( Fun S -> Rel S )
26 resdm 
 |-  ( Rel S -> ( S |` dom S ) = S )
27 24 25 26 3syl 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> ( S |` dom S ) = S )
28 20 27 syl5eq 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> ( Z |` dom S ) = S )
29 7 28 breqtrrd 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> ( X |` dom S )
30 simp1 
 |-  ( ( A C_ No /\ A e. _V /\ B e. _V ) -> A C_ No )
31 30 sselda 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> X e. No )
32 1 2 noetasuplem1 
 |-  ( ( A C_ No /\ A e. _V /\ B e. _V ) -> Z e. No )
33 32 adantr 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> Z e. No )
34 nodmon 
 |-  ( S e. No -> dom S e. On )
35 22 34 syl 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> dom S e. On )
36 sltres 
 |-  ( ( X e. No /\ Z e. No /\ dom S e. On ) -> ( ( X |` dom S )  X
37 31 33 35 36 syl3anc 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> ( ( X |` dom S )  X
38 29 37 mpd 
 |-  ( ( ( A C_ No /\ A e. _V /\ B e. _V ) /\ X e. A ) -> X