Metamath Proof Explorer

Theorem noetainflem3

Description: Lemma for noeta . W bounds B below . (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 noetainflem3 
|- ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> W

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 simpl2 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> B C_ No )
4 simpl3 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> B e. _V )
5 1 2 noetainflem2 
 |-  ( ( B C_ No /\ B e. _V ) -> ( W |` dom T ) = T )
6 3 4 5 syl2anc 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> ( W |` dom T ) = T )
7 simpr 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> Y e. B )
8 1 noinfbnd1 
 |-  ( ( B C_ No /\ B e. _V /\ Y e. B ) -> T
9 3 4 7 8 syl3anc 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> T
10 6 9 eqbrtrd 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> ( W |` dom T )
11 1 2 noetainflem1 
 |-  ( ( A e. _V /\ B C_ No /\ B e. _V ) -> W e. No )
12 11 adantr 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> W e. No )
13 simp2 
 |-  ( ( A e. _V /\ B C_ No /\ B e. _V ) -> B C_ No )
14 13 sselda 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> Y e. No )
15 1 noinfno 
 |-  ( ( B C_ No /\ B e. _V ) -> T e. No )
16 3 4 15 syl2anc 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> T e. No )
17 nodmon 
 |-  ( T e. No -> dom T e. On )
18 16 17 syl 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> dom T e. On )
19 sltres 
 |-  ( ( W e. No /\ Y e. No /\ dom T e. On ) -> ( ( W |` dom T )  W
20 12 14 18 19 syl3anc 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> ( ( W |` dom T )  W
21 10 20 mpd 
 |-  ( ( ( A e. _V /\ B C_ No /\ B e. _V ) /\ Y e. B ) -> W