Metamath Proof Explorer

Theorem nosupbnd1lem1

Description: Lemma for nosupbnd1 . Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupbnd1.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 ) ) ) )
Assertion nosupbnd1lem1 
|- ( ( -. E. x e. A A. y e. A -. x  -. S

Proof

Step Hyp Ref Expression
1 nosupbnd1.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 simp2l 
 |-  ( ( -. E. x e. A A. y e. A -. x  A C_ No )
3 simp3 
 |-  ( ( -. E. x e. A A. y e. A -. x  U e. A )
4 2 3 sseldd 
 |-  ( ( -. E. x e. A A. y e. A -. x  U e. No )
5 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
6 5 3ad2ant2 
 |-  ( ( -. E. x e. A A. y e. A -. x  S e. No )
7 nodmon 
 |-  ( S e. No -> dom S e. On )
8 6 7 syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom S e. On )
9 noreson 
 |-  ( ( U e. No /\ dom S e. On ) -> ( U |` dom S ) e. No )
10 4 8 9 syl2anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( U |` dom S ) e. No )
11 dmres 
 |-  dom ( U |` dom S ) = ( dom S i^i dom U )
12 inss1 
 |-  ( dom S i^i dom U ) C_ dom S
13 11 12 eqsstri 
 |-  dom ( U |` dom S ) C_ dom S
14 13 a1i 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom ( U |` dom S ) C_ dom S )
15 ssidd 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom S C_ dom S )
16 iffalse 
 |-  ( -. E. x e. A A. y e. A -. x  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 ) ) ) ) = ( 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 ) ) ) )
17 1 16 syl5eq 
 |-  ( -. E. x e. A A. y e. A -. x  S = ( 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 ) ) ) )
18 17 dmeqd 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = dom ( 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 ) ) ) )
19 iotaex 
 |-  ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) e. _V
20 eqid 
 |-  ( 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 ) ) ) = ( 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 ) ) )
21 19 20 dmmpti 
 |-  dom ( 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 ) ) ) = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) }
22 18 21 eqtrdi 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
23 22 eleq2d 
 |-  ( -. E. x e. A A. y e. A -. x  ( h e. dom S <-> h e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } ) )
24 vex 
 |-  h e. _V
25 eleq1w 
 |-  ( y = h -> ( y e. dom u <-> h e. dom u ) )
26 suceq 
 |-  ( y = h -> suc y = suc h )
27 26 reseq2d 
 |-  ( y = h -> ( u |` suc y ) = ( u |` suc h ) )
28 26 reseq2d 
 |-  ( y = h -> ( v |` suc y ) = ( v |` suc h ) )
29 27 28 eqeq12d 
 |-  ( y = h -> ( ( u |` suc y ) = ( v |` suc y ) <-> ( u |` suc h ) = ( v |` suc h ) ) )
30 29 imbi2d 
 |-  ( y = h -> ( ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> ( -. v  ( u |` suc h ) = ( v |` suc h ) ) ) )
31 30 ralbidv 
 |-  ( y = h -> ( A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) <-> A. v e. A ( -. v  ( u |` suc h ) = ( v |` suc h ) ) ) )
32 25 31 anbi12d 
 |-  ( y = h -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> ( h e. dom u /\ A. v e. A ( -. v  ( u |` suc h ) = ( v |` suc h ) ) ) ) )
33 32 rexbidv 
 |-  ( y = h -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. u e. A ( h e. dom u /\ A. v e. A ( -. v  ( u |` suc h ) = ( v |` suc h ) ) ) ) )
34 dmeq 
 |-  ( u = p -> dom u = dom p )
35 34 eleq2d 
 |-  ( u = p -> ( h e. dom u <-> h e. dom p ) )
36 breq2 
 |-  ( u = p -> ( v  v
37 36 notbid 
 |-  ( u = p -> ( -. v  -. v
38 reseq1 
 |-  ( u = p -> ( u |` suc h ) = ( p |` suc h ) )
39 38 eqeq1d 
 |-  ( u = p -> ( ( u |` suc h ) = ( v |` suc h ) <-> ( p |` suc h ) = ( v |` suc h ) ) )
40 37 39 imbi12d 
 |-  ( u = p -> ( ( -. v  ( u |` suc h ) = ( v |` suc h ) ) <-> ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) )
41 40 ralbidv 
 |-  ( u = p -> ( A. v e. A ( -. v  ( u |` suc h ) = ( v |` suc h ) ) <-> A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) )
42 35 41 anbi12d 
 |-  ( u = p -> ( ( h e. dom u /\ A. v e. A ( -. v  ( u |` suc h ) = ( v |` suc h ) ) ) <-> ( h e. dom p /\ A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) ) )
43 42 cbvrexvw 
 |-  ( E. u e. A ( h e. dom u /\ A. v e. A ( -. v  ( u |` suc h ) = ( v |` suc h ) ) ) <-> E. p e. A ( h e. dom p /\ A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) )
44 33 43 bitrdi 
 |-  ( y = h -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) <-> E. p e. A ( h e. dom p /\ A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) ) )
45 24 44 elab 
 |-  ( h e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } <-> E. p e. A ( h e. dom p /\ A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) )
46 23 45 bitrdi 
 |-  ( -. E. x e. A A. y e. A -. x  ( h e. dom S <-> E. p e. A ( h e. dom p /\ A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) ) )
47 46 3ad2ant1 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( h e. dom S <-> E. p e. A ( h e. dom p /\ A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) ) )
48 simpl1 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. E. x e. A A. y e. A -. x
49 simpl2 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( A C_ No /\ A e. _V ) )
50 simprl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> p e. A )
51 simprrl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> h e. dom p )
52 simprrr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) )
53 1 nosupres 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) -> ( S |` suc h ) = ( p |` suc h ) )
54 48 49 50 51 52 53 syl113anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( S |` suc h ) = ( p |` suc h ) )
55 simpl2l 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> A C_ No )
56 55 50 sseldd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> p e. No )
57 4 adantr 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> U e. No )
58 sltso 
 |-
59 soasym 
 |-  ( (  ( p  -. U
60 58 59 mpan 
 |-  ( ( p e. No /\ U e. No ) -> ( p  -. U
61 56 57 60 syl2anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( p  -. U
62 simpl3 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> U e. A )
63 breq1 
 |-  ( v = U -> ( v  U
64 63 notbid 
 |-  ( v = U -> ( -. v  -. U
65 reseq1 
 |-  ( v = U -> ( v |` suc h ) = ( U |` suc h ) )
66 65 eqeq2d 
 |-  ( v = U -> ( ( p |` suc h ) = ( v |` suc h ) <-> ( p |` suc h ) = ( U |` suc h ) ) )
67 64 66 imbi12d 
 |-  ( v = U -> ( ( -. v  ( p |` suc h ) = ( v |` suc h ) ) <-> ( -. U  ( p |` suc h ) = ( U |` suc h ) ) ) )
68 67 rspcv 
 |-  ( U e. A -> ( A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) -> ( -. U  ( p |` suc h ) = ( U |` suc h ) ) ) )
69 62 52 68 sylc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( -. U  ( p |` suc h ) = ( U |` suc h ) ) )
70 61 69 syld 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( p  ( p |` suc h ) = ( U |` suc h ) ) )
71 70 imp 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) /\ p  ( p |` suc h ) = ( U |` suc h ) )
72 nodmon 
 |-  ( p e. No -> dom p e. On )
73 56 72 syl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> dom p e. On )
74 onelon 
 |-  ( ( dom p e. On /\ h e. dom p ) -> h e. On )
75 73 51 74 syl2anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> h e. On )
76 sucelon 
 |-  ( h e. On <-> suc h e. On )
77 75 76 sylib 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> suc h e. On )
78 noreson 
 |-  ( ( U e. No /\ suc h e. On ) -> ( U |` suc h ) e. No )
79 57 77 78 syl2anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( U |` suc h ) e. No )
80 sonr 
 |-  ( (  -. ( U |` suc h )
81 58 80 mpan 
 |-  ( ( U |` suc h ) e. No -> -. ( U |` suc h )
82 79 81 syl 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. ( U |` suc h )
83 82 adantr 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) /\ p  -. ( U |` suc h )
84 71 83 eqnbrtrd 
 |-  ( ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) /\ p  -. ( p |` suc h )
85 84 ex 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( p  -. ( p |` suc h )
86 sltres 
 |-  ( ( p e. No /\ U e. No /\ suc h e. On ) -> ( ( p |` suc h )  p
87 56 57 77 86 syl3anc 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( ( p |` suc h )  p
88 87 con3d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> ( -. p  -. ( p |` suc h )
89 85 88 pm2.61d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. ( p |` suc h )
90 54 89 eqnbrtrd 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( p |` suc h ) = ( v |` suc h ) ) ) ) ) -> -. ( S |` suc h )
91 90 rexlimdvaa 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( E. p e. A ( h e. dom p /\ A. v e. A ( -. v  ( p |` suc h ) = ( v |` suc h ) ) ) -> -. ( S |` suc h )
92 47 91 sylbid 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( h e. dom S -> -. ( S |` suc h )
93 92 imp 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( S |` suc h )
94 nodmord 
 |-  ( S e. No -> Ord dom S )
95 ordsucss 
 |-  ( Ord dom S -> ( h e. dom S -> suc h C_ dom S ) )
96 6 94 95 3syl 
 |-  ( ( -. E. x e. A A. y e. A -. x  ( h e. dom S -> suc h C_ dom S ) )
97 96 imp 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  suc h C_ dom S )
98 97 resabs1d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( U |` dom S ) |` suc h ) = ( U |` suc h ) )
99 98 breq2d 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  ( ( S |` suc h )  ( S |` suc h )
100 93 99 mtbird 
 |-  ( ( ( -. E. x e. A A. y e. A -. x  -. ( S |` suc h )
101 100 ralrimiva 
 |-  ( ( -. E. x e. A A. y e. A -. x  A. h e. dom S -. ( S |` suc h )
102 noresle 
 |-  ( ( ( ( U |` dom S ) e. No /\ S e. No ) /\ ( dom ( U |` dom S ) C_ dom S /\ dom S C_ dom S /\ A. h e. dom S -. ( S |` suc h )  -. S
103 10 6 14 15 101 102 syl23anc 
 |-  ( ( -. E. x e. A A. y e. A -. x  -. S