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