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 onsucb 
 |-  ( 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 )