Metamath Proof Explorer


Theorem noinfbnd1lem1

Description: Lemma for noinfbnd1 . Establish a soft lower bound. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd1.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 ) ) ) )
Assertion noinfbnd1lem1
|- ( ( -. E. x e. B A. y e. B -. y  -. ( U |` dom T ) 

Proof

Step Hyp Ref Expression
1 noinfbnd1.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 1 noinfno
 |-  ( ( B C_ No /\ B e. V ) -> T e. No )
3 2 3ad2ant2
 |-  ( ( -. E. x e. B A. y e. B -. y  T e. No )
4 simp2l
 |-  ( ( -. E. x e. B A. y e. B -. y  B C_ No )
5 simp3
 |-  ( ( -. E. x e. B A. y e. B -. y  U e. B )
6 4 5 sseldd
 |-  ( ( -. E. x e. B A. y e. B -. y  U e. No )
7 nodmon
 |-  ( T e. No -> dom T e. On )
8 3 7 syl
 |-  ( ( -. E. x e. B A. y e. B -. y  dom T e. On )
9 noreson
 |-  ( ( U e. No /\ dom T e. On ) -> ( U |` dom T ) e. No )
10 6 8 9 syl2anc
 |-  ( ( -. E. x e. B A. y e. B -. y  ( U |` dom T ) e. No )
11 ssidd
 |-  ( ( -. E. x e. B A. y e. B -. y  dom T C_ dom T )
12 dmres
 |-  dom ( U |` dom T ) = ( dom T i^i dom U )
13 inss1
 |-  ( dom T i^i dom U ) C_ dom T
14 12 13 eqsstri
 |-  dom ( U |` dom T ) C_ dom T
15 14 a1i
 |-  ( ( -. E. x e. B A. y e. B -. y  dom ( U |` dom T ) C_ dom T )
16 nodmord
 |-  ( T e. No -> Ord dom T )
17 3 16 syl
 |-  ( ( -. E. x e. B A. y e. B -. y  Ord dom T )
18 ordsucss
 |-  ( Ord dom T -> ( h e. dom T -> suc h C_ dom T ) )
19 17 18 syl
 |-  ( ( -. E. x e. B A. y e. B -. y  ( h e. dom T -> suc h C_ dom T ) )
20 19 imp
 |-  ( ( ( -. E. x e. B A. y e. B -. y  suc h C_ dom T )
21 20 resabs1d
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( ( U |` dom T ) |` suc h ) = ( U |` suc h ) )
22 1 noinfdm
 |-  ( -. E. x e. B A. y e. B -. y  dom T = { h | E. p e. B ( h e. dom p /\ A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) ) } )
23 22 eleq2d
 |-  ( -. E. x e. B A. y e. B -. y  ( h e. dom T <-> h e. { h | E. p e. B ( h e. dom p /\ A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) ) } ) )
24 abid
 |-  ( h e. { h | E. p e. B ( h e. dom p /\ A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) ) } <-> E. p e. B ( h e. dom p /\ A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) ) )
25 breq2
 |-  ( q = v -> ( p  p 
26 25 notbid
 |-  ( q = v -> ( -. p  -. p 
27 reseq1
 |-  ( q = v -> ( q |` suc h ) = ( v |` suc h ) )
28 27 eqeq2d
 |-  ( q = v -> ( ( p |` suc h ) = ( q |` suc h ) <-> ( p |` suc h ) = ( v |` suc h ) ) )
29 26 28 imbi12d
 |-  ( q = v -> ( ( -. p  ( p |` suc h ) = ( q |` suc h ) ) <-> ( -. p  ( p |` suc h ) = ( v |` suc h ) ) ) )
30 29 cbvralvw
 |-  ( A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) <-> A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) )
31 30 anbi2i
 |-  ( ( h e. dom p /\ A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) ) <-> ( h e. dom p /\ A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) ) )
32 31 rexbii
 |-  ( E. p e. B ( h e. dom p /\ A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) ) <-> E. p e. B ( h e. dom p /\ A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) ) )
33 24 32 bitri
 |-  ( h e. { h | E. p e. B ( h e. dom p /\ A. q e. B ( -. p  ( p |` suc h ) = ( q |` suc h ) ) ) } <-> E. p e. B ( h e. dom p /\ A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) ) )
34 23 33 bitrdi
 |-  ( -. E. x e. B A. y e. B -. y  ( h e. dom T <-> E. p e. B ( h e. dom p /\ A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) ) ) )
35 34 3ad2ant1
 |-  ( ( -. E. x e. B A. y e. B -. y  ( h e. dom T <-> E. p e. B ( h e. dom p /\ A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) ) ) )
36 simpl2l
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> B C_ No )
37 simprl
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> p e. B )
38 36 37 sseldd
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> p e. No )
39 6 adantr
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> U e. No )
40 sltso
 |-  
41 soasym
 |-  ( (  ( p  -. U 
42 40 41 mpan
 |-  ( ( p e. No /\ U e. No ) -> ( p  -. U 
43 38 39 42 syl2anc
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( p  -. U 
44 nodmon
 |-  ( p e. No -> dom p e. On )
45 38 44 syl
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> dom p e. On )
46 simprrl
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> h e. dom p )
47 onelon
 |-  ( ( dom p e. On /\ h e. dom p ) -> h e. On )
48 45 46 47 syl2anc
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> h e. On )
49 sucelon
 |-  ( h e. On <-> suc h e. On )
50 48 49 sylib
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> suc h e. On )
51 sltres
 |-  ( ( U e. No /\ p e. No /\ suc h e. On ) -> ( ( U |` suc h )  U 
52 39 38 50 51 syl3anc
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( ( U |` suc h )  U 
53 43 52 nsyld
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( p  -. ( U |` suc h ) 
54 noreson
 |-  ( ( U e. No /\ suc h e. On ) -> ( U |` suc h ) e. No )
55 39 50 54 syl2anc
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( U |` suc h ) e. No )
56 sonr
 |-  ( (  -. ( U |` suc h ) 
57 40 56 mpan
 |-  ( ( U |` suc h ) e. No -> -. ( U |` suc h ) 
58 55 57 syl
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. ( U |` suc h ) 
59 58 adantr
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) /\ -. p  -. ( U |` suc h ) 
60 breq2
 |-  ( v = U -> ( p  p 
61 60 notbid
 |-  ( v = U -> ( -. p  -. p 
62 reseq1
 |-  ( v = U -> ( v |` suc h ) = ( U |` suc h ) )
63 62 eqeq2d
 |-  ( v = U -> ( ( p |` suc h ) = ( v |` suc h ) <-> ( p |` suc h ) = ( U |` suc h ) ) )
64 61 63 imbi12d
 |-  ( v = U -> ( ( -. p  ( p |` suc h ) = ( v |` suc h ) ) <-> ( -. p  ( p |` suc h ) = ( U |` suc h ) ) ) )
65 simprrr
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) )
66 simpl3
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> U e. B )
67 64 65 66 rspcdva
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( -. p  ( p |` suc h ) = ( U |` suc h ) ) )
68 67 imp
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) /\ -. p  ( p |` suc h ) = ( U |` suc h ) )
69 68 breq2d
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) /\ -. p  ( ( U |` suc h )  ( U |` suc h ) 
70 59 69 mtbird
 |-  ( ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) /\ -. p  -. ( U |` suc h ) 
71 70 ex
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( -. p  -. ( U |` suc h ) 
72 53 71 pm2.61d
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. ( U |` suc h ) 
73 simpl1
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. E. x e. B A. y e. B -. y 
74 simpl2
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( B C_ No /\ B e. V ) )
75 1 noinfres
 |-  ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) -> ( T |` suc h ) = ( p |` suc h ) )
76 73 74 37 46 65 75 syl113anc
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( T |` suc h ) = ( p |` suc h ) )
77 76 breq2d
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( ( U |` suc h )  ( U |` suc h ) 
78 72 77 mtbird
 |-  ( ( ( -. E. x e. B A. y e. B -. y  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. ( U |` suc h ) 
79 78 rexlimdvaa
 |-  ( ( -. E. x e. B A. y e. B -. y  ( E. p e. B ( h e. dom p /\ A. v e. B ( -. p  ( p |` suc h ) = ( v |` suc h ) ) ) -> -. ( U |` suc h ) 
80 35 79 sylbid
 |-  ( ( -. E. x e. B A. y e. B -. y  ( h e. dom T -> -. ( U |` suc h ) 
81 80 imp
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. ( U |` suc h ) 
82 21 81 eqnbrtrd
 |-  ( ( ( -. E. x e. B A. y e. B -. y  -. ( ( U |` dom T ) |` suc h ) 
83 82 ralrimiva
 |-  ( ( -. E. x e. B A. y e. B -. y  A. h e. dom T -. ( ( U |` dom T ) |` suc h ) 
84 noresle
 |-  ( ( ( T e. No /\ ( U |` dom T ) e. No ) /\ ( dom T C_ dom T /\ dom ( U |` dom T ) C_ dom T /\ A. h e. dom T -. ( ( U |` dom T ) |` suc h )  -. ( U |` dom T ) 
85 3 10 11 15 83 84 syl23anc
 |-  ( ( -. E. x e. B A. y e. B -. y  -. ( U |` dom T )